package coq-lsp

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val 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.

module Require : sig ... end

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

OCaml

Innovation. Community. Security.