diff --git a/coq-serapi/Extcoq/index.html b/coq-serapi/Extcoq/index.html index 42ef24fd..2681d224 100644 --- a/coq-serapi/Extcoq/index.html +++ b/coq-serapi/Extcoq/index.html @@ -1,2 +1,2 @@ -
Extcoq
Extcoq
Serapi.Ser_stream
Serapi.Ser_stream
Serapi.Serapi_assumptions
type t = {
predicative : bool;
type_in_type : bool;
vars : (Names.Id.t * Constr.t) list;
axioms : (Printer.axiom * Constr.t * ax_ctx) list;
opaque : (Names.Constant.t * Constr.t) list;
trans : (Names.Constant.t * Constr.t) list;
}
val build : Environ.env -> Constr.t Printer.ContextObjectMap.t -> t
val print : Environ.env -> Evd.evar_map -> t -> Pp.t
Serapi.Serapi_assumptions
type t = {
predicative : bool;
type_in_type : bool;
vars : (Names.Id.t * Constr.t) list;
axioms : (Printer.axiom * Constr.t * ax_ctx) list;
opaque : (Names.Constant.t * Constr.t) list;
trans : (Names.Constant.t * Constr.t) list;
}
val build : Environ.env -> Constr.t Printer.ContextObjectMap.t -> t
val print : Environ.env -> Evd.evar_map -> t -> Pp.t
Serapi.Serapi_doc
val save_vo :
+Serapi_doc (coq-serapi.Serapi.Serapi_doc) Module Serapi.Serapi_doc
val save_vo :
doc:Stm.doc ->
?ldir:Names.DirPath.t ->
pstate:Vernacstate.LemmaStack.t option ->
diff --git a/coq-serapi/Serapi/Serapi_goals/index.html b/coq-serapi/Serapi/Serapi_goals/index.html
index 897161b1..dd4b1474 100644
--- a/coq-serapi/Serapi/Serapi_goals/index.html
+++ b/coq-serapi/Serapi/Serapi_goals/index.html
@@ -1,5 +1,5 @@
-Serapi_goals (coq-serapi.Serapi.Serapi_goals) Module Serapi.Serapi_goals
val process_goal_gen :
+Serapi_goals (coq-serapi.Serapi.Serapi_goals) Module Serapi.Serapi_goals
val process_goal_gen :
(Environ.env -> Evd.evar_map -> Constr.t -> 'a) ->
Evd.evar_map ->
Evar.t ->
diff --git a/coq-serapi/Serapi/Serapi_paths/index.html b/coq-serapi/Serapi/Serapi_paths/index.html
index 9e80a055..73e95c48 100644
--- a/coq-serapi/Serapi/Serapi_paths/index.html
+++ b/coq-serapi/Serapi/Serapi_paths/index.html
@@ -1,5 +1,5 @@
-Serapi_paths (coq-serapi.Serapi.Serapi_paths) Module Serapi.Serapi_paths
val coq_loadpath_default :
+Serapi_paths (coq-serapi.Serapi.Serapi_paths) Module Serapi.Serapi_paths
diff --git a/coq-serapi/Serapi/Serapi_pp/index.html b/coq-serapi/Serapi/Serapi_pp/index.html
index 9dc01258..8f50d638 100644
--- a/coq-serapi/Serapi/Serapi_pp/index.html
+++ b/coq-serapi/Serapi/Serapi_pp/index.html
@@ -1,2 +1,2 @@
-Serapi_pp (coq-serapi.Serapi.Serapi_pp) Module Serapi.Serapi_pp
This module includes all of sertop custom Format-based printers for Coq datatypes.
We may want to split it into a library at some point and replace parts of Coq printing/
val pp_str : string pp
val pp_stateid : Stateid.t pp
val pp_feedback : Feedback.feedback pp
val pp_xml : Xml_datatype.xml pp
+Serapi_pp (coq-serapi.Serapi.Serapi_pp) Module Serapi.Serapi_pp
This module includes all of sertop custom Format-based printers for Coq datatypes.
We may want to split it into a library at some point and replace parts of Coq printing/
val pp_str : string pp
val pp_stateid : Stateid.t pp
val pp_feedback : Feedback.feedback pp
val pp_xml : Xml_datatype.xml pp
diff --git a/coq-serapi/Serapi/Serapi_protocol/ExnInfo/index.html b/coq-serapi/Serapi/Serapi_protocol/ExnInfo/index.html
index 6daa4ec5..155181b6 100644
--- a/coq-serapi/Serapi/Serapi_protocol/ExnInfo/index.html
+++ b/coq-serapi/Serapi/Serapi_protocol/ExnInfo/index.html
@@ -1,2 +1,2 @@
-ExnInfo (coq-serapi.Serapi.Serapi_protocol.ExnInfo) Module Serapi_protocol.ExnInfo
+ExnInfo (coq-serapi.Serapi.Serapi_protocol.ExnInfo) Module Serapi_protocol.ExnInfo
diff --git a/coq-serapi/Serapi/Serapi_protocol/QueryUtil/index.html b/coq-serapi/Serapi/Serapi_protocol/QueryUtil/index.html
index 323553d3..2a4622db 100644
--- a/coq-serapi/Serapi/Serapi_protocol/QueryUtil/index.html
+++ b/coq-serapi/Serapi/Serapi_protocol/QueryUtil/index.html
@@ -1,2 +1,2 @@
-QueryUtil (coq-serapi.Serapi.Serapi_protocol.QueryUtil) Module Serapi_protocol.QueryUtil
val info_of_id : Environ.env -> string -> coq_object list * coq_object list
+QueryUtil (coq-serapi.Serapi.Serapi_protocol.QueryUtil) Module Serapi_protocol.QueryUtil
val info_of_id : Environ.env -> string -> coq_object list * coq_object list
diff --git a/coq-serapi/Serapi/Serapi_protocol/State/index.html b/coq-serapi/Serapi/Serapi_protocol/State/index.html
index d4b7a5fc..8f929a40 100644
--- a/coq-serapi/Serapi/Serapi_protocol/State/index.html
+++ b/coq-serapi/Serapi/Serapi_protocol/State/index.html
@@ -1,2 +1,2 @@
-State (coq-serapi.Serapi.Serapi_protocol.State) Module Serapi_protocol.State
val make : ?in_file:string -> ?ldir:Names.DirPath.t -> unit -> t
Create a state and possibly initialize Coq with an input_file
+State (coq-serapi.Serapi.Serapi_protocol.State) Module Serapi_protocol.State
val make : ?in_file:string -> ?ldir:Names.DirPath.t -> unit -> t
Create a state and possibly initialize Coq with an input_file
diff --git a/coq-serapi/Serapi/Serapi_protocol/index.html b/coq-serapi/Serapi/Serapi_protocol/index.html
index 6238bb7e..5cdd9674 100644
--- a/coq-serapi/Serapi/Serapi_protocol/index.html
+++ b/coq-serapi/Serapi/Serapi_protocol/index.html
@@ -1,4 +1,4 @@
-Serapi_protocol (coq-serapi.Serapi.Serapi_protocol) Module Serapi.Serapi_protocol
The SerAPI Protocol
SerAPI is a set of utilities designed to help users and tool creators to interact with Coq in a systematic way; in particular, SerAPI was designed to provide full serialization and de-serialization of key Coq structures, including user-level AST and kernel terms.
SerAPI also provides a reification of Coq's document building API, making it pretty easy to build and check systematically Coq documents.
As of today SerAPI does provide the following components:
serlib
: A library providing serializers for core Coq structures; the main serialization formats are S-expressions and JSON. serlib
is based on ppx_sexp_conv from Jane Street and `ppx_deriving_yojson`. serlib
also provides for custom hash and equality functions for many Coq types.sertop
: A toplevel executable exposing a simple document building and querying protocol. This is the main component, we document it properly below.sercomp
: A simple compiler utility for .v files that can input and output Coq files in a variety of formats. See its manual for more help.serload
: TODO
History:
SerAPI was a JsCoq offspring project; JsCoq added experimental serialization of Coq terms, however we quickly realized that this facility would be helpful in the general setting; we also took advantage of the serialization facilities to specify the Coq building API as a DSL; the client for the tool was an experimental Emacs mode by Clément Pit-Claudel.
The next step was to provide reliable "round-trip" (de)serialization of full Coq documents; Karl Palmskog contributed the round trip testing infrastructure to make this happen.
Users:
SerAPI is a bit of a swiss army knife, in the sense that it is a general "talk to Coq" tool and can do many things; a good way to understand the tool is look at some of its users, see the list of them in the Project's README
Basic Overview of the Protocol:
SerAPI protocol can be divided in two main sets of operations: document creation and checking, and document querying.
Note that the protocol is fully specified as a DSL written in OCaml; thus, its canonical specification can be found below as documents to the OCaml code. In this section, we attempt a brief introduction, but the advanced user will without doubt want to look at the details just below.
Document creation and checking:
Before you can use SerAPI to extract any information about a Coq document, you must indeed have Coq parse and process the document. Coq's parsing process is quite complicated due to user-extensibility, but SerAPI tries to smooth the experience as much as possible.
A Coq document is basically a list of sentences which are uniquely identified by a Stateid.t
object; for our purposes this identifier is an integer.
Note: In future versions, sentence id will be deprecated, and instead we will use Language Server Protocol-style locations inside the document to identify sentences.
Each sentence has a "parent", that is to say, a previous sentence; the initial sentence has as a parent sid = 1
(sid
= sentence id).
Note that the parent is important for parsing as it may modify the parsing itself, for example it may be a Notation
command.
Thus, to build or append to a Coq document, you should select a parent sentence and ask SerAPI to add some new ones. This is achieved with the (Add (opts) "text")
command.
See below for a detailed overview of Add
, but the basic idea is that Coq will parse and add to the current document as many sentences as you have sent to it. Unfortunately, sentence number for the newly added ones is not always predictable but there are workarounds for that.
If succesfull, Add
will send back an Added
message with the location and new sentence identifier. This is useful to let SerAPI do the splitting of sentences for you. A typical use thus is:
(Add () "Lemma addnC n : n + 0 = n. Proof. now induction n. Qed.")
This will return 4 answers.
Sentence Checking
Adding a set of sentences basically amounts to parsing, however in most cases Coq won't try to typecheck or run the tactics at hand. For that purpose you can use the (Exec sid)
command. Taking a sentence id, Check
will actually check sid
and all the sentences sid
depends upon.
Note that in some modes Coq can skip proofs here, so in order to get a fully-checked document you may have to issue Check
for every sentence on it. Checking a sentence twice is usually a noop.
Modification of the Document
In order to modify a "live" document, SerAPI does provide a (Cancel sid)
command. Cancel
will take a sentence id and return the list of sentences that are not valid anymore.
Thus, you can edit a document by cancelling and re-adding sentences.
Caveats
Cancelling a non-executed part is poorly supported by the underlying Coq checking algorithm. In particular, Cancel
will force execution up to the previous sentence; thus it is not possible to parse a list of sentences and then replace them without incurring in the cost of executing them. In particular, it could be even the case that after issuing Cancel sid
, there is an error in the execution of an unrelated sentence. It should be possible to identify this sentence using the exception attributes. As of today, this remains a hard-limitation of the STM.
Querying documents:
For a particular point on the document, you can query Coq for information about it. Common query use cases are for example lists of tactics, AST, completion, etc... Querying is done using the (Query (opts) query)
command. The full specification can be found below.
A particulary of Query
is that the caller must set all the pertinent output options. For example, if the query should return for-humans data or machine-readable one.
Non-interactive use
In many cases, non-interactive use is very convenient; for that, we recommend you read the help of the `sercomp` compiler.
Protocol Specification
Basic Protocol Objects
SerAPI can return different kinds of objects as an answer to queries; object type is usually distinguished by a tag, for example (CoqString "foo")
or (CoqConstr (App ...)
Serialization representation is derived from the OCaml representation automatically, except for a few custom datatypes (see below). Thus, the best is to use Merlin or some OCaml-browsing tool as to know the internal of each type; we provide a brief description of each object:
type coq_object =
| CoqString of string
(*A string
*)| CoqSList of string list
(*A list of strings
*)| CoqPp of Pp.t
(*A Coq "Pretty Printing" Document type, main type used by Coq to submit formatted output
*)| CoqLoc of Loc.t
(*A Coq Location object, used for positions inside the document.
*)| CoqTok of Tok.t CAst.t list
(*Coq Tokens, as produced by the lexer
*)| CoqDP of Names.DirPath.t
(*Coq "Logical" Paths, used for module and section names
*)| CoqAst of Vernacexpr.vernac_control
(*Coq Abstract Syntax trees for statements, as produced by the parser
*)| CoqOption of Goptions.option_name * Goptions.option_state
(*Coq Options, as in Set Resolution Depth
*)| CoqConstr of Constr.constr
(*Coq Kernel terms, this is the fundamental representation for terms of the Calculus of Inductive constructions
*)| CoqEConstr of EConstr.t
(*Coq Kernel terms, but maybe open
*)| CoqExpr of Constrexpr.constr_expr
(*Coq term ASTs, this is the user-level parsing tree of terms
*)| CoqMInd of Names.MutInd.t * Declarations.mutual_inductive_body
(*Coq kernel-level inductive; this is a low-level object that contains all the details of an inductive.
*)| CoqEnv of Environ.env
(*Coq kernel-level enviroments: they do provide the full information about what the kernel know, heavy.
*)| CoqTactic of Names.KerName.t * Ltac_plugin.Tacenv.ltac_entry
(*Representation of an Ltac tactic definition
*)| CoqLtac of Ltac_plugin.Tacexpr.raw_tactic_expr
(*AST of an LTAC tactic definition
*)| CoqGenArg of Genarg.raw_generic_argument
(*Coq Generic argument, can contain any type
*)| CoqQualId of Libnames.qualid
(*Qualified identifier
*)| CoqGlobRef of Names.GlobRef.t
(*"Global Reference", which is a type that can point to a module, a constant, a variable, a constructor...
*)| CoqGlobRefExt of Globnames.extended_global_reference
(*"Extended Global Reference", as they can contain syntactic definitions too
*)| CoqImplicit of Impargs.implicits_list
(*Implicit status for a constant
*)| CoqProfData of Ltac_plugin.Profile_ltac.treenode
(*Ltac Profiler data
*)| CoqNotation of Constrexpr.notation
(*Representation of a notation (usually a string)
*)| CoqUnparsing of Ppextend.notation_printing_rules
+Serapi_protocol (coq-serapi.Serapi.Serapi_protocol) Module Serapi.Serapi_protocol
The SerAPI Protocol
SerAPI is a set of utilities designed to help users and tool creators to interact with Coq in a systematic way; in particular, SerAPI was designed to provide full serialization and de-serialization of key Coq structures, including user-level AST and kernel terms.
SerAPI also provides a reification of Coq's document building API, making it pretty easy to build and check systematically Coq documents.
As of today SerAPI does provide the following components:
serlib
: A library providing serializers for core Coq structures; the main serialization formats are S-expressions and JSON. serlib
is based on ppx_sexp_conv from Jane Street and `ppx_deriving_yojson`. serlib
also provides for custom hash and equality functions for many Coq types.sertop
: A toplevel executable exposing a simple document building and querying protocol. This is the main component, we document it properly below.sercomp
: A simple compiler utility for .v files that can input and output Coq files in a variety of formats. See its manual for more help.serload
: TODO
History:
SerAPI was a JsCoq offspring project; JsCoq added experimental serialization of Coq terms, however we quickly realized that this facility would be helpful in the general setting; we also took advantage of the serialization facilities to specify the Coq building API as a DSL; the client for the tool was an experimental Emacs mode by Clément Pit-Claudel.
The next step was to provide reliable "round-trip" (de)serialization of full Coq documents; Karl Palmskog contributed the round trip testing infrastructure to make this happen.
Users:
SerAPI is a bit of a swiss army knife, in the sense that it is a general "talk to Coq" tool and can do many things; a good way to understand the tool is look at some of its users, see the list of them in the Project's README
Basic Overview of the Protocol:
SerAPI protocol can be divided in two main sets of operations: document creation and checking, and document querying.
Note that the protocol is fully specified as a DSL written in OCaml; thus, its canonical specification can be found below as documents to the OCaml code. In this section, we attempt a brief introduction, but the advanced user will without doubt want to look at the details just below.
Document creation and checking:
Before you can use SerAPI to extract any information about a Coq document, you must indeed have Coq parse and process the document. Coq's parsing process is quite complicated due to user-extensibility, but SerAPI tries to smooth the experience as much as possible.
A Coq document is basically a list of sentences which are uniquely identified by a Stateid.t
object; for our purposes this identifier is an integer.
Note: In future versions, sentence id will be deprecated, and instead we will use Language Server Protocol-style locations inside the document to identify sentences.
Each sentence has a "parent", that is to say, a previous sentence; the initial sentence has as a parent sid = 1
(sid
= sentence id).
Note that the parent is important for parsing as it may modify the parsing itself, for example it may be a Notation
command.
Thus, to build or append to a Coq document, you should select a parent sentence and ask SerAPI to add some new ones. This is achieved with the (Add (opts) "text")
command.
See below for a detailed overview of Add
, but the basic idea is that Coq will parse and add to the current document as many sentences as you have sent to it. Unfortunately, sentence number for the newly added ones is not always predictable but there are workarounds for that.
If succesfull, Add
will send back an Added
message with the location and new sentence identifier. This is useful to let SerAPI do the splitting of sentences for you. A typical use thus is:
(Add () "Lemma addnC n : n + 0 = n. Proof. now induction n. Qed.")
This will return 4 answers.
Sentence Checking
Adding a set of sentences basically amounts to parsing, however in most cases Coq won't try to typecheck or run the tactics at hand. For that purpose you can use the (Exec sid)
command. Taking a sentence id, Check
will actually check sid
and all the sentences sid
depends upon.
Note that in some modes Coq can skip proofs here, so in order to get a fully-checked document you may have to issue Check
for every sentence on it. Checking a sentence twice is usually a noop.
Modification of the Document
In order to modify a "live" document, SerAPI does provide a (Cancel sid)
command. Cancel
will take a sentence id and return the list of sentences that are not valid anymore.
Thus, you can edit a document by cancelling and re-adding sentences.
Caveats
Cancelling a non-executed part is poorly supported by the underlying Coq checking algorithm. In particular, Cancel
will force execution up to the previous sentence; thus it is not possible to parse a list of sentences and then replace them without incurring in the cost of executing them. In particular, it could be even the case that after issuing Cancel sid
, there is an error in the execution of an unrelated sentence. It should be possible to identify this sentence using the exception attributes. As of today, this remains a hard-limitation of the STM.
Querying documents:
For a particular point on the document, you can query Coq for information about it. Common query use cases are for example lists of tactics, AST, completion, etc... Querying is done using the (Query (opts) query)
command. The full specification can be found below.
A particulary of Query
is that the caller must set all the pertinent output options. For example, if the query should return for-humans data or machine-readable one.
Non-interactive use
In many cases, non-interactive use is very convenient; for that, we recommend you read the help of the `sercomp` compiler.
Protocol Specification
Basic Protocol Objects
SerAPI can return different kinds of objects as an answer to queries; object type is usually distinguished by a tag, for example (CoqString "foo")
or (CoqConstr (App ...)
Serialization representation is derived from the OCaml representation automatically, except for a few custom datatypes (see below). Thus, the best is to use Merlin or some OCaml-browsing tool as to know the internal of each type; we provide a brief description of each object:
type coq_object =
| CoqString of string
(*A string
*)| CoqSList of string list
(*A list of strings
*)| CoqPp of Pp.t
(*A Coq "Pretty Printing" Document type, main type used by Coq to submit formatted output
*)| CoqLoc of Loc.t
(*A Coq Location object, used for positions inside the document.
*)| CoqTok of Tok.t CAst.t list
(*Coq Tokens, as produced by the lexer
*)| CoqDP of Names.DirPath.t
(*Coq "Logical" Paths, used for module and section names
*)| CoqAst of Vernacexpr.vernac_control
(*Coq Abstract Syntax trees for statements, as produced by the parser
*)| CoqOption of Goptions.option_name * Goptions.option_state
(*Coq Options, as in Set Resolution Depth
*)| CoqConstr of Constr.constr
(*Coq Kernel terms, this is the fundamental representation for terms of the Calculus of Inductive constructions
*)| CoqEConstr of EConstr.t
(*Coq Kernel terms, but maybe open
*)| CoqExpr of Constrexpr.constr_expr
(*Coq term ASTs, this is the user-level parsing tree of terms
*)| CoqMInd of Names.MutInd.t * Declarations.mutual_inductive_body
(*Coq kernel-level inductive; this is a low-level object that contains all the details of an inductive.
*)| CoqEnv of Environ.env
(*Coq kernel-level enviroments: they do provide the full information about what the kernel know, heavy.
*)| CoqTactic of Names.KerName.t * Ltac_plugin.Tacenv.ltac_entry
(*Representation of an Ltac tactic definition
*)| CoqLtac of Ltac_plugin.Tacexpr.raw_tactic_expr
(*AST of an LTAC tactic definition
*)| CoqGenArg of Genarg.raw_generic_argument
(*Coq Generic argument, can contain any type
*)| CoqQualId of Libnames.qualid
(*Qualified identifier
*)| CoqGlobRef of Names.GlobRef.t
(*"Global Reference", which is a type that can point to a module, a constant, a variable, a constructor...
*)| CoqGlobRefExt of Globnames.extended_global_reference
(*"Extended Global Reference", as they can contain syntactic definitions too
*)| CoqImplicit of Impargs.implicits_list
(*Implicit status for a constant
*)| CoqProfData of Ltac_plugin.Profile_ltac.treenode
(*Ltac Profiler data
*)| CoqNotation of Constrexpr.notation
(*Representation of a notation (usually a string)
*)| CoqUnparsing of Ppextend.notation_printing_rules
* Notation_gram.notation_grammar
(*Rules for notation printing and some internals
*)| CoqGoal of Constr.t Serapi_goals.reified_goal Serapi_goals.ser_goals
(*Goals, with types and terms in Kernel-level representation
*)| CoqExtGoal of Constrexpr.constr_expr Serapi_goals.reified_goal
- Serapi_goals.ser_goals
(*Goals, with types and terms in user-level, AST representation
*)| CoqProof of EConstr.constr list
(*Proof object: really low-level and likely to be deprecated.
*)| CoqAssumptions of Serapi_assumptions.t
(*Structured representation of the assumptions of a constant.
*)| CoqComments of ((int * int) * string) list list
(*List of comments in a document, the list will have one element for each call to Add
; note that with the current model, it is hard to do better, as a call to Add
can map to several sentences so comments are really mapped to each of those.
See https://github.com/coq/coq/issues/12413 for updates on improved support
*)| CoqLibObjects of {
}
(*Meta-logical Objects in Coq's library / module system
*)
There are some Coq types that cannot be seralizaled properly, in this case, the types can be "opaque", or we will perform some manual serialization, such for GADTs.
In the past generic arguments were such a case, but that has been fixed in SerAPI 0.17. Please open an issue or pull request if you find such a discrepancy as to document it here.
Printing Options
type format_opt = {
pp_format : print_format;
(*Output format (default PpSer)
*)pp_depth : int;
(*Depth (default 0)
*)pp_elide : string;
(*Elipsis (default: "...")
*)pp_margin : int;
(*Margin (default: 72)
*)
}
Printing options, not all options are relevant for all printing backends
type print_opt = {
sid : Stateid.t;
(*sid
denotes the sentence id we are querying over, essential information as goals for example will vary.
*)pp : format_opt;
(*Printing format of the query, this can be used to select the type of the answer, as for example to show goals in human-form.
*)
}
val gen_pp_obj : Environ.env -> Evd.evar_map -> coq_object -> Pp.t
Query Sub-Protocol
Predicates on the queries. This is at the moment mostly a token functionality
type query_opt = {
preds : query_pred list;
(*List of predicates on queries, mostly a placeholder, will allow to add filtering conditions in the future
*)limit : int option;
(*Limit the number of results, should evolve into an API with resume functionality, maybe we adopt LSP conventions here
*)sid : Stateid.t;
(*sid
denotes the sentence id we are querying over, essential information as goals for example will vary.
*)pp : format_opt;
(*Printing format of the query, this can be used to select the type of the answer, as for example to show goals in human-form.
*)route : Feedback.route_id;
(*Legacy/Deprecated STM query method
*)
}
Query options, note the default values that help interactive use, however in mechanized use we do not recommend skipping any field
type query_cmd =
| Option
(*List of options Coq knows about
*)| Search
(*Query version of the Search
command
*)| Goals
(*Current goals, in kernel form
*)| EGoals
(*Current goals, in AST form
*)| Ast
(*Ast for the current sentence
*)| TypeOf of string
(*Type of an expression (unimplemented?)
*)| Names of string
(*(Names prefix)
will return the list of identifiers Coq knows that start with prefix
*)| Tactics of string
(*(Tactcis prefix)
will return the list of tactics Coq knows that start with prefix
*)| Locate of string
(*Query version of the Locate
commands
*)| Implicits of string
(*Return information of implicits for a given constant
*)| Unparsing of string
(*Return internal information for a given notation
*)| Definition of string
(*Return the definition for a given global
*)| LogicalPath of string
(*Returns Coq's "logical path" for a given file
*)| PNotations
(*Return a list of notations
*)| ProfileData
(*Return LTAC profile data, if any
*)| Proof
(*Return the proof object low-level
*)| Vernac of string
(*Execute an arbitrary Coq command in an isolated state.
*)| Env
(*Return the current enviroment
*)| Assumptions of string
(*Return the assumptions of a given global
*)| Complete of string
(*Naïve but efficient prefix-based completion of identifiers
*)| Comments
(*Get all comments of a document
*)| Objects
(*Get Coq meta-logical module objects
*)
Query commands are mostly a tag and some arguments determining the result type.
Important Note that Query
won't force execution of a particular state, thus for example if you do (Query ((sid 3)) Goals)
and the sentence 3
wasn't evaluated, then the query will return zero answers.
We would ideally evolve towards a true query language, likley having query_cmd
and coq_object
be typed such that query : 'a query -> 'a coq_object.
module QueryUtil : sig ... end
Control Sub-Protocol
Adding a new sentence
parse ontop
of the given sentence with entry entry
type add_opts = {
lim : int option;
(*Parse lim
sentences at most (None
== no limit)
*)ontop : Stateid.t option;
(*parse ontop
of the given sentence
*)newtip : Stateid.t option;
(*Make newtip
the new sentence id, very useful to avoid synchronous operations
*)verb : bool;
(*verb
internal Coq parameter, be verbose on parsing
*)
}
Add
will take a string and parse all the sentences on it, until an error of the end is found. Options for Add
are:
Creating a new document
experimental
type newdoc_opts = {
top_name : Coqargs.top;
(*name of the top-level module of the new document
*)ml_load_path : string list option;
(*Initial ML loadpath
*)vo_load_path : Loadpath.vo_path list option;
(*Initial LoadPath for the document
*)require_libs : Coqargs.require_injection list option;
(*Libraries to load in the initial document state
*)
}
type save_opts = {
prefix_output_dir : string option;
(*prefix a directory to the saved vo file.
*)sid : Stateid.t;
(*sid of the point to save the document
*)
}
Save options, Coq must save a module `Foo` to a concrete module path determined by -R / -Q options , so we don't have a lot of choice here.
Top Level Protocol
The top level protocol is the main input command to SerAPI, we detail each of the commands below.
The main interaction loop is as: 1. submit tagged command (tag (Cmd args))
2. receive tagged ack (Answer tag Ack)
3. receive tagged results, usually (Answer tag (ObjList ...)
or (Answer tag (CoqExn ...)
4. receive tagged completion event (Answer tag Completed)
The Ack
and Completed
events are always produced, and provide a kind of "bracking" for command execution.
type cmd =
| NewDoc of newdoc_opts
(*Create a new document, experimental, only usable when --no_init
was used.
*)| SaveDoc of save_opts
(*Save the .vo file corresponding to the current document, note that proofs must be closed etc... in order for this to succeed.
*)| Add of add_opts * string
(*Add a set of sentences to the current document
*)| Cancel of Stateid.t list
(*Remove a set of sentences from the current document
*)| Exec of Stateid.t
(*Execute a particular sentence
*)| Query of query_opt * query_cmd
(*Query a Coq document
*)| Print of print_opt * coq_object
(*Print some object
*)| Parse of parse_opt * string
(*Parse
*)| Join
(*Be sure that a document is consistent
*)| Finish
(*Internal
*)| ReadFile of string
| Tokenize of string
| Noop
| Help
Each top level command will produce an answers, see below for answer description.
module ExnInfo : sig ... end
type answer_kind =
| Ack
(*The command was received, Coq is processing it.
*)| Completed
(*The command was completed.
*)| Added of Stateid.t * Loc.t * Stm.add_focus
(*A sentence was added, with corresponding sentence id and location.
*)| Canceled of Stateid.t list
(*A set of sentences are not valid anymore.
*)| ObjList of coq_object list
(*Set of objects, usually the answer to a query
*)| CoqExn of ExnInfo.t
(*The command produced an error, optionally at a document location
*)
State of the evaluator
module State : sig ... end
Entry points to the DSL evaluator
val exec_cmd : State.t -> cmd -> answer_kind list * State.t
exec_cmd cmd
execute SerAPI command
We introduce our own feedback type to overcome some limitations of Coq's Feedback, for now we only modify the Message data
type feedback = {
doc_id : Feedback.doc_id;
span_id : Stateid.t;
route : Feedback.route_id;
contents : feedback_content;
}
type answer =
| Answer of cmd_tag * answer_kind
(*The answer is comming from a user-issued command
*)| Feedback of feedback
(*Output produced by Coq (asynchronously)
*)
General answers of the protocol can be responses to commands, or Coq messages
+ Serapi_goals.ser_goals
(*Goals, with types and terms in user-level, AST representation
*)| CoqProof of EConstr.constr list
(*Proof object: really low-level and likely to be deprecated.
*)| CoqAssumptions of Serapi_assumptions.t
(*Structured representation of the assumptions of a constant.
*)| CoqComments of ((int * int) * string) list list
(*List of comments in a document, the list will have one element for each call to Add
; note that with the current model, it is hard to do better, as a call to Add
can map to several sentences so comments are really mapped to each of those.
See https://github.com/coq/coq/issues/12413 for updates on improved support
*)| CoqLibObjects of {
}
(*Meta-logical Objects in Coq's library / module system
*)
There are some Coq types that cannot be seralizaled properly, in this case, the types can be "opaque", or we will perform some manual serialization, such for GADTs.
In the past generic arguments were such a case, but that has been fixed in SerAPI 0.17. Please open an issue or pull request if you find such a discrepancy as to document it here.
Printing Options
type format_opt = {
pp_format : print_format;
(*Output format (default PpSer)
*)pp_depth : int;
(*Depth (default 0)
*)pp_elide : string;
(*Elipsis (default: "...")
*)pp_margin : int;
(*Margin (default: 72)
*)
}
Printing options, not all options are relevant for all printing backends
type print_opt = {
sid : Stateid.t;
(*sid
denotes the sentence id we are querying over, essential information as goals for example will vary.
*)pp : format_opt;
(*Printing format of the query, this can be used to select the type of the answer, as for example to show goals in human-form.
*)
}
val gen_pp_obj : Environ.env -> Evd.evar_map -> coq_object -> Pp.t
Query Sub-Protocol
Predicates on the queries. This is at the moment mostly a token functionality
type query_opt = {
preds : query_pred list;
(*List of predicates on queries, mostly a placeholder, will allow to add filtering conditions in the future
*)limit : int option;
(*Limit the number of results, should evolve into an API with resume functionality, maybe we adopt LSP conventions here
*)sid : Stateid.t;
(*sid
denotes the sentence id we are querying over, essential information as goals for example will vary.
*)pp : format_opt;
(*Printing format of the query, this can be used to select the type of the answer, as for example to show goals in human-form.
*)route : Feedback.route_id;
(*Legacy/Deprecated STM query method
*)
}
Query options, note the default values that help interactive use, however in mechanized use we do not recommend skipping any field
type query_cmd =
| Option
(*List of options Coq knows about
*)| Search
(*Query version of the Search
command
*)| Goals
(*Current goals, in kernel form
*)| EGoals
(*Current goals, in AST form
*)| Ast
(*Ast for the current sentence
*)| TypeOf of string
(*Type of an expression (unimplemented?)
*)| Names of string
(*(Names prefix)
will return the list of identifiers Coq knows that start with prefix
*)| Tactics of string
(*(Tactcis prefix)
will return the list of tactics Coq knows that start with prefix
*)| Locate of string
(*Query version of the Locate
commands
*)| Implicits of string
(*Return information of implicits for a given constant
*)| Unparsing of string
(*Return internal information for a given notation
*)| Definition of string
(*Return the definition for a given global
*)| LogicalPath of string
(*Returns Coq's "logical path" for a given file
*)| PNotations
(*Return a list of notations
*)| ProfileData
(*Return LTAC profile data, if any
*)| Proof
(*Return the proof object low-level
*)| Vernac of string
(*Execute an arbitrary Coq command in an isolated state.
*)| Env
(*Return the current enviroment
*)| Assumptions of string
(*Return the assumptions of a given global
*)| Complete of string
(*Naïve but efficient prefix-based completion of identifiers
*)| Comments
(*Get all comments of a document
*)| Objects
(*Get Coq meta-logical module objects
*)
Query commands are mostly a tag and some arguments determining the result type.
Important Note that Query
won't force execution of a particular state, thus for example if you do (Query ((sid 3)) Goals)
and the sentence 3
wasn't evaluated, then the query will return zero answers.
We would ideally evolve towards a true query language, likley having query_cmd
and coq_object
be typed such that query : 'a query -> 'a coq_object.
module QueryUtil : sig ... end
Control Sub-Protocol
Adding a new sentence
parse ontop
of the given sentence with entry entry
type add_opts = {
lim : int option;
(*Parse lim
sentences at most (None
== no limit)
*)ontop : Stateid.t option;
(*parse ontop
of the given sentence
*)newtip : Stateid.t option;
(*Make newtip
the new sentence id, very useful to avoid synchronous operations
*)verb : bool;
(*verb
internal Coq parameter, be verbose on parsing
*)
}
Add
will take a string and parse all the sentences on it, until an error of the end is found. Options for Add
are:
Creating a new document
experimental
type newdoc_opts = {
top_name : Coqargs.top;
(*name of the top-level module of the new document
*)ml_load_path : string list option;
(*Initial ML loadpath
*)vo_load_path : Loadpath.vo_path list option;
(*Initial LoadPath for the document
*)require_libs : (string * string option * Lib.export_flag option) list option;
(*Libraries to load in the initial document state
*)
}
type save_opts = {
prefix_output_dir : string option;
(*prefix a directory to the saved vo file.
*)sid : Stateid.t;
(*sid of the point to save the document
*)
}
Save options, Coq must save a module `Foo` to a concrete module path determined by -R / -Q options , so we don't have a lot of choice here.
Top Level Protocol
The top level protocol is the main input command to SerAPI, we detail each of the commands below.
The main interaction loop is as: 1. submit tagged command (tag (Cmd args))
2. receive tagged ack (Answer tag Ack)
3. receive tagged results, usually (Answer tag (ObjList ...)
or (Answer tag (CoqExn ...)
4. receive tagged completion event (Answer tag Completed)
The Ack
and Completed
events are always produced, and provide a kind of "bracking" for command execution.
type cmd =
| NewDoc of newdoc_opts
(*Create a new document, experimental, only usable when --no_init
was used.
*)| SaveDoc of save_opts
(*Save the .vo file corresponding to the current document, note that proofs must be closed etc... in order for this to succeed.
*)| Add of add_opts * string
(*Add a set of sentences to the current document
*)| Cancel of Stateid.t list
(*Remove a set of sentences from the current document
*)| Exec of Stateid.t
(*Execute a particular sentence
*)| Query of query_opt * query_cmd
(*Query a Coq document
*)| Print of print_opt * coq_object
(*Print some object
*)| Parse of parse_opt * string
(*Parse
*)| Join
(*Be sure that a document is consistent
*)| Finish
(*Internal
*)| ReadFile of string
| Tokenize of string
| Noop
| Help
Each top level command will produce an answers, see below for answer description.
module ExnInfo : sig ... end
type answer_kind =
| Ack
(*The command was received, Coq is processing it.
*)| Completed
(*The command was completed.
*)| Added of Stateid.t * Loc.t * Stm.add_focus
(*A sentence was added, with corresponding sentence id and location.
*)| Canceled of Stateid.t list
(*A set of sentences are not valid anymore.
*)| ObjList of coq_object list
(*Set of objects, usually the answer to a query
*)| CoqExn of ExnInfo.t
(*The command produced an error, optionally at a document location
*)
State of the evaluator
module State : sig ... end
Entry points to the DSL evaluator
val exec_cmd : State.t -> cmd -> answer_kind list * State.t
exec_cmd cmd
execute SerAPI command
We introduce our own feedback type to overcome some limitations of Coq's Feedback, for now we only modify the Message data
type feedback = {
doc_id : Feedback.doc_id;
span_id : Stateid.t;
route : Feedback.route_id;
contents : feedback_content;
}
type answer =
| Answer of cmd_tag * answer_kind
(*The answer is comming from a user-issued command
*)| Feedback of feedback
(*Output produced by Coq (asynchronously)
*)
General answers of the protocol can be responses to commands, or Coq messages
diff --git a/coq-serapi/Serapi/index.html b/coq-serapi/Serapi/index.html
index cd0b65ae..38ee94ee 100644
--- a/coq-serapi/Serapi/index.html
+++ b/coq-serapi/Serapi/index.html
@@ -1,2 +1,2 @@
-Serapi (coq-serapi.Serapi) Module Serapi
module Ser_stream : sig ... end
module Serapi_assumptions : sig ... end
module Serapi_doc : sig ... end
module Serapi_goals : sig ... end
module Serapi_paths : sig ... end
module Serapi_pp : sig ... end
This module includes all of sertop custom Format-based printers for Coq datatypes.
module Serapi_protocol : sig ... end
The SerAPI Protocol
+Serapi (coq-serapi.Serapi) Module Serapi
module Ser_stream : sig ... end
module Serapi_assumptions : sig ... end
module Serapi_doc : sig ... end
module Serapi_goals : sig ... end
module Serapi_paths : sig ... end
module Serapi_pp : sig ... end
This module includes all of sertop custom Format-based printers for Coq datatypes.
module Serapi_protocol : sig ... end
The SerAPI Protocol
diff --git a/coq-serapi/Serlib/SerType/Biject/argument-1-M/index.html b/coq-serapi/Serlib/SerType/Biject/argument-1-M/index.html
index a07f93ab..47a8499e 100644
--- a/coq-serapi/Serlib/SerType/Biject/argument-1-M/index.html
+++ b/coq-serapi/Serlib/SerType/Biject/argument-1-M/index.html
@@ -1,5 +1,5 @@
-M (coq-serapi.Serlib.SerType.Biject.M) Parameter Biject.M
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : _t -> Sexplib0.Sexp.t
val _t_of_sexp : Sexplib0.Sexp.t -> _t
val hash_fold__t :
+M (coq-serapi.Serlib.SerType.Biject.M) Parameter Biject.M
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : _t -> Sexplib0.Sexp.t
val _t_of_sexp : Sexplib0.Sexp.t -> _t
val hash_fold__t :
Ppx_hash_lib.Std.Hash.state ->
_t ->
Ppx_hash_lib.Std.Hash.state
val hash__t : _t -> Ppx_hash_lib.Std.Hash.hash_value
diff --git a/coq-serapi/Serlib/SerType/Biject/index.html b/coq-serapi/Serlib/SerType/Biject/index.html
index aca2e268..bb8a8f2c 100644
--- a/coq-serapi/Serlib/SerType/Biject/index.html
+++ b/coq-serapi/Serlib/SerType/Biject/index.html
@@ -1,2 +1,2 @@
-Biject (coq-serapi.Serlib.SerType.Biject) Module SerType.Biject
Parameters
module M : Bijectable
Signature
type t = M.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
+Biject (coq-serapi.Serlib.SerType.Biject) Module SerType.Biject
Parameters
module M : Bijectable
Signature
type t = M.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
diff --git a/coq-serapi/Serlib/SerType/Biject1/argument-1-M/index.html b/coq-serapi/Serlib/SerType/Biject1/argument-1-M/index.html
index 7cb7ff83..16c5a4e4 100644
--- a/coq-serapi/Serlib/SerType/Biject1/argument-1-M/index.html
+++ b/coq-serapi/Serlib/SerType/Biject1/argument-1-M/index.html
@@ -1,5 +1,5 @@
-M (coq-serapi.Serlib.SerType.Biject1.M) Parameter Biject1.M
val _t_to_yojson : ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
+M (coq-serapi.Serlib.SerType.Biject1.M) Parameter Biject1.M
val _t_to_yojson : ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : ('a -> Sexplib0.Sexp.t) -> 'a _t -> Sexplib0.Sexp.t
val _t_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a _t
val hash_fold__t :
diff --git a/coq-serapi/Serlib/SerType/Biject1/index.html b/coq-serapi/Serlib/SerType/Biject1/index.html
index 8bc62a50..5a50de41 100644
--- a/coq-serapi/Serlib/SerType/Biject1/index.html
+++ b/coq-serapi/Serlib/SerType/Biject1/index.html
@@ -1,5 +1,5 @@
-Biject1 (coq-serapi.Serlib.SerType.Biject1) Module SerType.Biject1
Parameters
module M : Bijectable1
Signature
type 'a t = 'a M.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
+Biject1 (coq-serapi.Serlib.SerType.Biject1) Module SerType.Biject1
Parameters
module M : Bijectable1
Signature
type 'a t = 'a M.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a t Ppx_deriving_yojson_runtime.error_or
include Ppx_hash_lib.Hashable.S1 with type 'a t := 'a t
val hash_fold_t :
diff --git a/coq-serapi/Serlib/SerType/Opaque/argument-1-M/index.html b/coq-serapi/Serlib/SerType/Opaque/argument-1-M/index.html
index 820d1099..f53bcf60 100644
--- a/coq-serapi/Serlib/SerType/Opaque/argument-1-M/index.html
+++ b/coq-serapi/Serlib/SerType/Opaque/argument-1-M/index.html
@@ -1,2 +1,2 @@
-M (coq-serapi.Serlib.SerType.Opaque.M) Parameter Opaque.M
+M (coq-serapi.Serlib.SerType.Opaque.M) Parameter Opaque.M
diff --git a/coq-serapi/Serlib/SerType/Opaque/index.html b/coq-serapi/Serlib/SerType/Opaque/index.html
index 6ed98dac..c97ab7dd 100644
--- a/coq-serapi/Serlib/SerType/Opaque/index.html
+++ b/coq-serapi/Serlib/SerType/Opaque/index.html
@@ -1,2 +1,2 @@
-Opaque (coq-serapi.Serlib.SerType.Opaque) Module SerType.Opaque
Parameters
module M : OpaqueDesc
Signature
type t = M.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
+Opaque (coq-serapi.Serlib.SerType.Opaque) Module SerType.Opaque
Parameters
module M : OpaqueDesc
Signature
type t = M.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
diff --git a/coq-serapi/Serlib/SerType/Opaque1/argument-1-M/index.html b/coq-serapi/Serlib/SerType/Opaque1/argument-1-M/index.html
index 0f648f4c..f32fc796 100644
--- a/coq-serapi/Serlib/SerType/Opaque1/argument-1-M/index.html
+++ b/coq-serapi/Serlib/SerType/Opaque1/argument-1-M/index.html
@@ -1,2 +1,2 @@
-M (coq-serapi.Serlib.SerType.Opaque1.M) Parameter Opaque1.M
+M (coq-serapi.Serlib.SerType.Opaque1.M) Parameter Opaque1.M
diff --git a/coq-serapi/Serlib/SerType/Opaque1/index.html b/coq-serapi/Serlib/SerType/Opaque1/index.html
index 6c255ee9..5bcf8c6b 100644
--- a/coq-serapi/Serlib/SerType/Opaque1/index.html
+++ b/coq-serapi/Serlib/SerType/Opaque1/index.html
@@ -1,5 +1,5 @@
-Opaque1 (coq-serapi.Serlib.SerType.Opaque1) Module SerType.Opaque1
Parameters
module M : OpaqueDesc1
Signature
type 'a t = 'a M.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
+Opaque1 (coq-serapi.Serlib.SerType.Opaque1) Module SerType.Opaque1
Parameters
module M : OpaqueDesc1
Signature
type 'a t = 'a M.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a t Ppx_deriving_yojson_runtime.error_or
include Ppx_hash_lib.Hashable.S1 with type 'a t := 'a t
val hash_fold_t :
diff --git a/coq-serapi/Serlib/SerType/Pierce/argument-1-M/index.html b/coq-serapi/Serlib/SerType/Pierce/argument-1-M/index.html
index 22ec491f..b9d61c85 100644
--- a/coq-serapi/Serlib/SerType/Pierce/argument-1-M/index.html
+++ b/coq-serapi/Serlib/SerType/Pierce/argument-1-M/index.html
@@ -1,5 +1,5 @@
-M (coq-serapi.Serlib.SerType.Pierce.M) Parameter Pierce.M
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : _t -> Sexplib0.Sexp.t
val _t_of_sexp : Sexplib0.Sexp.t -> _t
val hash_fold__t :
+M (coq-serapi.Serlib.SerType.Pierce.M) Parameter Pierce.M
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : _t -> Sexplib0.Sexp.t
val _t_of_sexp : Sexplib0.Sexp.t -> _t
val hash_fold__t :
Ppx_hash_lib.Std.Hash.state ->
_t ->
Ppx_hash_lib.Std.Hash.state
val hash__t : _t -> Ppx_hash_lib.Std.Hash.hash_value
diff --git a/coq-serapi/Serlib/SerType/Pierce/index.html b/coq-serapi/Serlib/SerType/Pierce/index.html
index 5cf782d7..b4afc6e2 100644
--- a/coq-serapi/Serlib/SerType/Pierce/index.html
+++ b/coq-serapi/Serlib/SerType/Pierce/index.html
@@ -1,2 +1,2 @@
-Pierce (coq-serapi.Serlib.SerType.Pierce) Module SerType.Pierce
Parameters
module M : Pierceable
Signature
type t = M.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
+Pierce (coq-serapi.Serlib.SerType.Pierce) Module SerType.Pierce
Parameters
module M : Pierceable
Signature
type t = M.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
diff --git a/coq-serapi/Serlib/SerType/Pierce1/argument-1-M/index.html b/coq-serapi/Serlib/SerType/Pierce1/argument-1-M/index.html
index bdd64a44..03fab92a 100644
--- a/coq-serapi/Serlib/SerType/Pierce1/argument-1-M/index.html
+++ b/coq-serapi/Serlib/SerType/Pierce1/argument-1-M/index.html
@@ -1,5 +1,5 @@
-M (coq-serapi.Serlib.SerType.Pierce1.M) Parameter Pierce1.M
val _t_to_yojson : ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
+M (coq-serapi.Serlib.SerType.Pierce1.M) Parameter Pierce1.M
val _t_to_yojson : ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : ('a -> Sexplib0.Sexp.t) -> 'a _t -> Sexplib0.Sexp.t
val _t_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a _t
val hash_fold__t :
diff --git a/coq-serapi/Serlib/SerType/Pierce1/index.html b/coq-serapi/Serlib/SerType/Pierce1/index.html
index a66afd6d..555b8c81 100644
--- a/coq-serapi/Serlib/SerType/Pierce1/index.html
+++ b/coq-serapi/Serlib/SerType/Pierce1/index.html
@@ -1,5 +1,5 @@
-Pierce1 (coq-serapi.Serlib.SerType.Pierce1) Module SerType.Pierce1
Parameters
module M : Pierceable1
Signature
type 'a t = 'a M.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
+Pierce1 (coq-serapi.Serlib.SerType.Pierce1) Module SerType.Pierce1
Parameters
module M : Pierceable1
Signature
type 'a t = 'a M.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a t Ppx_deriving_yojson_runtime.error_or
include Ppx_hash_lib.Hashable.S1 with type 'a t := 'a t
val hash_fold_t :
diff --git a/coq-serapi/Serlib/SerType/index.html b/coq-serapi/Serlib/SerType/index.html
index b7f44aed..3bc4b222 100644
--- a/coq-serapi/Serlib/SerType/index.html
+++ b/coq-serapi/Serlib/SerType/index.html
@@ -1,2 +1,2 @@
-SerType (coq-serapi.Serlib.SerType) Module Serlib.SerType
module type SJHC = sig ... end
module type SJHC1 = sig ... end
module type Bijectable = sig ... end
Bijection with serializable types
module type Bijectable1 = sig ... end
module type Pierceable = sig ... end
module type Pierceable1 = sig ... end
module type OpaqueDesc = sig ... end
module type OpaqueDesc1 = sig ... end
+SerType (coq-serapi.Serlib.SerType) Module Serlib.SerType
module type SJHC = sig ... end
module type SJHC1 = sig ... end
module type Bijectable = sig ... end
Bijection with serializable types
module type Bijectable1 = sig ... end
module type Pierceable = sig ... end
module type Pierceable1 = sig ... end
module type OpaqueDesc = sig ... end
module type OpaqueDesc1 = sig ... end
diff --git a/coq-serapi/Serlib/SerType/module-type-Bijectable/index.html b/coq-serapi/Serlib/SerType/module-type-Bijectable/index.html
index 849d670d..de152723 100644
--- a/coq-serapi/Serlib/SerType/module-type-Bijectable/index.html
+++ b/coq-serapi/Serlib/SerType/module-type-Bijectable/index.html
@@ -1,5 +1,5 @@
-Bijectable (coq-serapi.Serlib.SerType.Bijectable) Module type SerType.Bijectable
Bijection with serializable types
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : _t -> Sexplib0.Sexp.t
val _t_of_sexp : Sexplib0.Sexp.t -> _t
val hash_fold__t :
+Bijectable (coq-serapi.Serlib.SerType.Bijectable) Module type SerType.Bijectable
Bijection with serializable types
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : _t -> Sexplib0.Sexp.t
val _t_of_sexp : Sexplib0.Sexp.t -> _t
val hash_fold__t :
Ppx_hash_lib.Std.Hash.state ->
_t ->
Ppx_hash_lib.Std.Hash.state
val hash__t : _t -> Ppx_hash_lib.Std.Hash.hash_value
diff --git a/coq-serapi/Serlib/SerType/module-type-Bijectable1/index.html b/coq-serapi/Serlib/SerType/module-type-Bijectable1/index.html
index 854a3fd3..602d6885 100644
--- a/coq-serapi/Serlib/SerType/module-type-Bijectable1/index.html
+++ b/coq-serapi/Serlib/SerType/module-type-Bijectable1/index.html
@@ -1,5 +1,5 @@
-Bijectable1 (coq-serapi.Serlib.SerType.Bijectable1) Module type SerType.Bijectable1
val _t_to_yojson : ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
+Bijectable1 (coq-serapi.Serlib.SerType.Bijectable1) Module type SerType.Bijectable1
val _t_to_yojson : ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : ('a -> Sexplib0.Sexp.t) -> 'a _t -> Sexplib0.Sexp.t
val _t_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a _t
val hash_fold__t :
diff --git a/coq-serapi/Serlib/SerType/module-type-OpaqueDesc/index.html b/coq-serapi/Serlib/SerType/module-type-OpaqueDesc/index.html
index 863ab44f..4a9e4cf9 100644
--- a/coq-serapi/Serlib/SerType/module-type-OpaqueDesc/index.html
+++ b/coq-serapi/Serlib/SerType/module-type-OpaqueDesc/index.html
@@ -1,2 +1,2 @@
-OpaqueDesc (coq-serapi.Serlib.SerType.OpaqueDesc) Module type SerType.OpaqueDesc
+OpaqueDesc (coq-serapi.Serlib.SerType.OpaqueDesc) Module type SerType.OpaqueDesc
diff --git a/coq-serapi/Serlib/SerType/module-type-OpaqueDesc1/index.html b/coq-serapi/Serlib/SerType/module-type-OpaqueDesc1/index.html
index 00a84f2d..c406ed89 100644
--- a/coq-serapi/Serlib/SerType/module-type-OpaqueDesc1/index.html
+++ b/coq-serapi/Serlib/SerType/module-type-OpaqueDesc1/index.html
@@ -1,2 +1,2 @@
-OpaqueDesc1 (coq-serapi.Serlib.SerType.OpaqueDesc1) Module type SerType.OpaqueDesc1
+OpaqueDesc1 (coq-serapi.Serlib.SerType.OpaqueDesc1) Module type SerType.OpaqueDesc1
diff --git a/coq-serapi/Serlib/SerType/module-type-Pierceable/index.html b/coq-serapi/Serlib/SerType/module-type-Pierceable/index.html
index c5f1bc93..f0b6e270 100644
--- a/coq-serapi/Serlib/SerType/module-type-Pierceable/index.html
+++ b/coq-serapi/Serlib/SerType/module-type-Pierceable/index.html
@@ -1,5 +1,5 @@
-Pierceable (coq-serapi.Serlib.SerType.Pierceable) Module type SerType.Pierceable
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : _t -> Sexplib0.Sexp.t
val _t_of_sexp : Sexplib0.Sexp.t -> _t
val hash_fold__t :
+Pierceable (coq-serapi.Serlib.SerType.Pierceable) Module type SerType.Pierceable
val _t_to_yojson : _t -> Yojson.Safe.t
val _t_of_yojson : Yojson.Safe.t -> _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : _t -> Sexplib0.Sexp.t
val _t_of_sexp : Sexplib0.Sexp.t -> _t
val hash_fold__t :
Ppx_hash_lib.Std.Hash.state ->
_t ->
Ppx_hash_lib.Std.Hash.state
val hash__t : _t -> Ppx_hash_lib.Std.Hash.hash_value
diff --git a/coq-serapi/Serlib/SerType/module-type-Pierceable1/index.html b/coq-serapi/Serlib/SerType/module-type-Pierceable1/index.html
index 354de256..40f58ad9 100644
--- a/coq-serapi/Serlib/SerType/module-type-Pierceable1/index.html
+++ b/coq-serapi/Serlib/SerType/module-type-Pierceable1/index.html
@@ -1,5 +1,5 @@
-Pierceable1 (coq-serapi.Serlib.SerType.Pierceable1) Module type SerType.Pierceable1
val _t_to_yojson : ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
+Pierceable1 (coq-serapi.Serlib.SerType.Pierceable1) Module type SerType.Pierceable1
val _t_to_yojson : ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a _t Ppx_deriving_yojson_runtime.error_or
val sexp_of__t : ('a -> Sexplib0.Sexp.t) -> 'a _t -> Sexplib0.Sexp.t
val _t_of_sexp : (Sexplib0.Sexp.t -> 'a) -> Sexplib0.Sexp.t -> 'a _t
val hash_fold__t :
diff --git a/coq-serapi/Serlib/SerType/module-type-SJHC/index.html b/coq-serapi/Serlib/SerType/module-type-SJHC/index.html
index 5535b380..09f8eb0c 100644
--- a/coq-serapi/Serlib/SerType/module-type-SJHC/index.html
+++ b/coq-serapi/Serlib/SerType/module-type-SJHC/index.html
@@ -1,2 +1,2 @@
-SJHC (coq-serapi.Serlib.SerType.SJHC) Module type SerType.SJHC
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
+SJHC (coq-serapi.Serlib.SerType.SJHC) Module type SerType.SJHC
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
diff --git a/coq-serapi/Serlib/SerType/module-type-SJHC1/index.html b/coq-serapi/Serlib/SerType/module-type-SJHC1/index.html
index 34258912..c0f88260 100644
--- a/coq-serapi/Serlib/SerType/module-type-SJHC1/index.html
+++ b/coq-serapi/Serlib/SerType/module-type-SJHC1/index.html
@@ -1,5 +1,5 @@
-SJHC1 (coq-serapi.Serlib.SerType.SJHC1) Module type SerType.SJHC1
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
+SJHC1 (coq-serapi.Serlib.SerType.SJHC1) Module type SerType.SJHC1
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a t Ppx_deriving_yojson_runtime.error_or
include Ppx_hash_lib.Hashable.S1 with type 'a t := 'a t
val hash_fold_t :
diff --git a/coq-serapi/Serlib/Ser_attributes/index.html b/coq-serapi/Serlib/Ser_attributes/index.html
index 8998bc3a..9e60be2e 100644
--- a/coq-serapi/Serlib/Ser_attributes/index.html
+++ b/coq-serapi/Serlib/Ser_attributes/index.html
@@ -1,5 +1,5 @@
-Ser_attributes (coq-serapi.Serlib.Ser_attributes) Module Serlib.Ser_attributes
module CAst = Ser_cAst
val vernac_flag_type_to_yojson : vernac_flag_type -> Yojson.Safe.t
val vernac_flag_type_of_yojson :
+Ser_attributes (coq-serapi.Serlib.Ser_attributes) Module Serlib.Ser_attributes
module CAst = Ser_cAst
val vernac_flag_type_to_yojson : vernac_flag_type -> Yojson.Safe.t
val vernac_flag_type_of_yojson :
Yojson.Safe.t ->
vernac_flag_type Ppx_deriving_yojson_runtime.error_or
val vernac_flag_type_of_sexp : Sexplib0.Sexp.t -> vernac_flag_type
val sexp_of_vernac_flag_type : vernac_flag_type -> Sexplib0.Sexp.t
val hash_fold_vernac_flag_type :
Ppx_hash_lib.Std.Hash.state ->
diff --git a/coq-serapi/Serlib/Ser_cAst/index.html b/coq-serapi/Serlib/Ser_cAst/index.html
index febad86c..fd9ee46b 100644
--- a/coq-serapi/Serlib/Ser_cAst/index.html
+++ b/coq-serapi/Serlib/Ser_cAst/index.html
@@ -1,5 +1,5 @@
-Ser_cAst (coq-serapi.Serlib.Ser_cAst) Module Serlib.Ser_cAst
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
+Ser_cAst (coq-serapi.Serlib.Ser_cAst) Module Serlib.Ser_cAst
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a t Ppx_deriving_yojson_runtime.error_or
include Ppx_hash_lib.Hashable.S1 with type 'a t := 'a t
val hash_fold_t :
diff --git a/coq-serapi/Serlib/Ser_cEphemeron/B/index.html b/coq-serapi/Serlib/Ser_cEphemeron/B/index.html
index fcf49816..1bb8f5d0 100644
--- a/coq-serapi/Serlib/Ser_cEphemeron/B/index.html
+++ b/coq-serapi/Serlib/Ser_cEphemeron/B/index.html
@@ -1,5 +1,5 @@
-B (coq-serapi.Serlib.Ser_cEphemeron.B) Module Ser_cEphemeron.B
type 'a t = 'a EBiject.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
+B (coq-serapi.Serlib.Ser_cEphemeron.B) Module Ser_cEphemeron.B
type 'a t = 'a EBiject.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a t Ppx_deriving_yojson_runtime.error_or
val t_of_sexp : (Sexplib0__.Sexp.t -> 'a) -> Sexplib0__.Sexp.t -> 'a t
val sexp_of_t : ('a -> Sexplib0__.Sexp.t) -> 'a t -> Sexplib0__.Sexp.t
val hash_fold_t :
diff --git a/coq-serapi/Serlib/Ser_cEphemeron/EBiject/index.html b/coq-serapi/Serlib/Ser_cEphemeron/EBiject/index.html
index 3572f3a4..7f459136 100644
--- a/coq-serapi/Serlib/Ser_cEphemeron/EBiject/index.html
+++ b/coq-serapi/Serlib/Ser_cEphemeron/EBiject/index.html
@@ -1,5 +1,5 @@
-EBiject (coq-serapi.Serlib.Ser_cEphemeron.EBiject) Module Ser_cEphemeron.EBiject
val _t_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
+EBiject (coq-serapi.Serlib.Ser_cEphemeron.EBiject) Module Ser_cEphemeron.EBiject
val _t_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a _t Ppx_deriving_yojson_runtime.error_or
val _ :
diff --git a/coq-serapi/Serlib/Ser_cEphemeron/index.html b/coq-serapi/Serlib/Ser_cEphemeron/index.html
index 22491f10..336230e7 100644
--- a/coq-serapi/Serlib/Ser_cEphemeron/index.html
+++ b/coq-serapi/Serlib/Ser_cEphemeron/index.html
@@ -1,5 +1,5 @@
-Ser_cEphemeron (coq-serapi.Serlib.Ser_cEphemeron) Module Serlib.Ser_cEphemeron
module EBiject : sig ... end
module B : sig ... end
type 'a key = 'a B.t
val key_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a key -> Yojson.Safe.t
val key_of_yojson :
+Ser_cEphemeron (coq-serapi.Serlib.Ser_cEphemeron) Module Serlib.Ser_cEphemeron
module EBiject : sig ... end
module B : sig ... end
type 'a key = 'a B.t
val key_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a key -> Yojson.Safe.t
val key_of_yojson :
'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a key Ppx_deriving_yojson_runtime.error_or
val _ :
diff --git a/coq-serapi/Serlib/Ser_cMap/Make/argument-2-S/index.html b/coq-serapi/Serlib/Ser_cMap/Make/argument-2-S/index.html
index f0405e72..cf9b2150 100644
--- a/coq-serapi/Serlib/Ser_cMap/Make/argument-2-S/index.html
+++ b/coq-serapi/Serlib/Ser_cMap/Make/argument-2-S/index.html
@@ -1,2 +1,2 @@
-S (coq-serapi.Serlib.Ser_cMap.Make.S) Parameter Make.S
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
+S (coq-serapi.Serlib.Ser_cMap.Make.S) Parameter Make.S
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
diff --git a/coq-serapi/Serlib/Ser_cMap/Make/index.html b/coq-serapi/Serlib/Ser_cMap/Make/index.html
index 55750f8c..b5677f74 100644
--- a/coq-serapi/Serlib/Ser_cMap/Make/index.html
+++ b/coq-serapi/Serlib/Ser_cMap/Make/index.html
@@ -1,5 +1,5 @@
-Make (coq-serapi.Serlib.Ser_cMap.Make) Module Ser_cMap.Make
Parameters
module S : SerType.SJHC with type t = M.key
Signature
include CSig.MapS with type key = M.key with type 'a t = 'a M.t
val empty : 'a t
val is_empty : 'a t -> bool
val merge :
+Make (coq-serapi.Serlib.Ser_cMap.Make) Module Ser_cMap.Make
Parameters
module S : SerType.SJHC with type t = M.key
Signature
include CSig.MapS with type key = M.key with type 'a t = 'a M.t
val empty : 'a t
val is_empty : 'a t -> bool
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t ->
'b t ->
diff --git a/coq-serapi/Serlib/Ser_cMap/index.html b/coq-serapi/Serlib/Ser_cMap/index.html
index c5614479..c5cc5660 100644
--- a/coq-serapi/Serlib/Ser_cMap/index.html
+++ b/coq-serapi/Serlib/Ser_cMap/index.html
@@ -1,5 +1,5 @@
-Ser_cMap (coq-serapi.Serlib.Ser_cMap) Module Serlib.Ser_cMap
module type ExtS = sig ... end
module Make
+Ser_cMap (coq-serapi.Serlib.Ser_cMap) Module Serlib.Ser_cMap
module type ExtS = sig ... end
diff --git a/coq-serapi/Serlib/Ser_cMap/module-type-ExtS/index.html b/coq-serapi/Serlib/Ser_cMap/module-type-ExtS/index.html
index 02022b5b..91ca8108 100644
--- a/coq-serapi/Serlib/Ser_cMap/module-type-ExtS/index.html
+++ b/coq-serapi/Serlib/Ser_cMap/module-type-ExtS/index.html
@@ -1,5 +1,5 @@
-ExtS (coq-serapi.Serlib.Ser_cMap.ExtS) Module type Ser_cMap.ExtS
include CSig.MapS
val empty : 'a t
val is_empty : 'a t -> bool
val merge :
+ExtS (coq-serapi.Serlib.Ser_cMap.ExtS) Module type Ser_cMap.ExtS
include CSig.MapS
val empty : 'a t
val is_empty : 'a t -> bool
val merge :
(key -> 'a option -> 'b option -> 'c option) ->
'a t ->
'b t ->
diff --git a/coq-serapi/Serlib/Ser_cPrimitives/OOTP/index.html b/coq-serapi/Serlib/Ser_cPrimitives/OOTP/index.html
index 0f3f9a6a..c7c0a999 100644
--- a/coq-serapi/Serlib/Ser_cPrimitives/OOTP/index.html
+++ b/coq-serapi/Serlib/Ser_cPrimitives/OOTP/index.html
@@ -1,5 +1,5 @@
-OOTP (coq-serapi.Serlib.Ser_cPrimitives.OOTP) Module Ser_cPrimitives.OOTP
val ptype_to_yojson : ptype -> Yojson.Safe.t
val ptype_of_yojson :
+OOTP (coq-serapi.Serlib.Ser_cPrimitives.OOTP) Module Ser_cPrimitives.OOTP
val ptype_to_yojson : ptype -> Yojson.Safe.t
val ptype_of_yojson :
Yojson.Safe.t ->
ptype Ppx_deriving_yojson_runtime.error_or
val ptype_of_sexp : Sexplib0.Sexp.t -> ptype
val sexp_of_ptype : ptype -> Sexplib0.Sexp.t
val hash_fold_ptype :
Ppx_hash_lib.Std.Hash.state ->
diff --git a/coq-serapi/Serlib/Ser_cPrimitives/Op_or_type_/index.html b/coq-serapi/Serlib/Ser_cPrimitives/Op_or_type_/index.html
index ab532d1c..f067d1ac 100644
--- a/coq-serapi/Serlib/Ser_cPrimitives/Op_or_type_/index.html
+++ b/coq-serapi/Serlib/Ser_cPrimitives/Op_or_type_/index.html
@@ -1,2 +1,2 @@
-Op_or_type_ (coq-serapi.Serlib.Ser_cPrimitives.Op_or_type_) Module Ser_cPrimitives.Op_or_type_
type t = OOTP.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
val hash_fold_t : t Base__Ppx_hash_lib.hash_fold
val hash : t -> Base__Ppx_hash_lib.Std.Hash.hash_value
val compare : t Base__Ppx_compare_lib.compare
+Op_or_type_ (coq-serapi.Serlib.Ser_cPrimitives.Op_or_type_) Module Ser_cPrimitives.Op_or_type_
type t = OOTP.t
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
val hash_fold_t : t Base__Ppx_hash_lib.hash_fold
val hash : t -> Base__Ppx_hash_lib.Std.Hash.hash_value
val compare : t Base__Ppx_compare_lib.compare
diff --git a/coq-serapi/Serlib/Ser_cPrimitives/PTP/index.html b/coq-serapi/Serlib/Ser_cPrimitives/PTP/index.html
index 450978fb..57a87148 100644
--- a/coq-serapi/Serlib/Ser_cPrimitives/PTP/index.html
+++ b/coq-serapi/Serlib/Ser_cPrimitives/PTP/index.html
@@ -1,5 +1,5 @@
-PTP (coq-serapi.Serlib.Ser_cPrimitives.PTP) Module Ser_cPrimitives.PTP
val _t_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
+PTP (coq-serapi.Serlib.Ser_cPrimitives.PTP) Module Ser_cPrimitives.PTP
val _t_to_yojson : 'a. ('a -> Yojson.Safe.t) -> 'a _t -> Yojson.Safe.t
val _t_of_yojson :
'a. (Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a _t Ppx_deriving_yojson_runtime.error_or
val _ :
diff --git a/coq-serapi/Serlib/Ser_cPrimitives/Prim_type_/index.html b/coq-serapi/Serlib/Ser_cPrimitives/Prim_type_/index.html
index 6d4bbfba..670200a8 100644
--- a/coq-serapi/Serlib/Ser_cPrimitives/Prim_type_/index.html
+++ b/coq-serapi/Serlib/Ser_cPrimitives/Prim_type_/index.html
@@ -1,5 +1,5 @@
-Prim_type_ (coq-serapi.Serlib.Ser_cPrimitives.Prim_type_) Module Ser_cPrimitives.Prim_type_
type 'a t = 'a PTP.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
+Prim_type_ (coq-serapi.Serlib.Ser_cPrimitives.Prim_type_) Module Ser_cPrimitives.Prim_type_
type 'a t = 'a PTP.t
val to_yojson : ('a -> Yojson.Safe.t) -> 'a t -> Yojson.Safe.t
val of_yojson :
(Yojson.Safe.t -> 'a Ppx_deriving_yojson_runtime.error_or) ->
Yojson.Safe.t ->
'a t Ppx_deriving_yojson_runtime.error_or
val t_of_sexp : (Sexplib0__.Sexp.t -> 'a) -> Sexplib0__.Sexp.t -> 'a t
val sexp_of_t : ('a -> Sexplib0__.Sexp.t) -> 'a t -> Sexplib0__.Sexp.t
val hash_fold_t :
diff --git a/coq-serapi/Serlib/Ser_cPrimitives/index.html b/coq-serapi/Serlib/Ser_cPrimitives/index.html
index 8f3bd420..3e1a0580 100644
--- a/coq-serapi/Serlib/Ser_cPrimitives/index.html
+++ b/coq-serapi/Serlib/Ser_cPrimitives/index.html
@@ -1,5 +1,5 @@
-Ser_cPrimitives (coq-serapi.Serlib.Ser_cPrimitives) Module Serlib.Ser_cPrimitives