package coq-lsp

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

  • to make the read-effect dependency explicit
  • to workaround the lack of a pure interface in Coq
val interp : token:Limits.Token.t -> intern:Library.Intern.t -> st:State.t -> Files.t -> Ast.Require.t -> (State.t, Loc.t) Protect.E.t
OCaml

Innovation. Community. Security.