Module Coq.InterpSource

Sourceval interp : token:Limits.Token.t -> intern:unit -> st:State.t -> Ast.t -> (State.t, Loc.t) Protect.E.t

Intepretation of "pure" Coq commands, that is to say, commands that are assumed not to interact with the file-system, etc... Note these commands will be memoized.

Sourcemodule Require : sig ... end

Interpretation of "require". We wrap this function for two reasons: