aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-29 09:56:37 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-04-29 09:56:37 +0000
commitf73d7c4614d000f068550b5144d80b7eceed58e9 (patch)
tree4fa9a679a6e55269cc5c7cf24fce725acb2574b5 /kernel
parent552e596e81362e348fc17fcebcc428005934bed6 (diff)
Move from ocamlweb to ocamdoc to generate mli documentation
dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.mli85
-rw-r--r--kernel/cbytegen.mli8
-rw-r--r--kernel/cemitcodes.mli5
-rw-r--r--kernel/closure.mli78
-rw-r--r--kernel/conv_oracle.mli24
-rw-r--r--kernel/cooking.mli18
-rw-r--r--kernel/declarations.mli132
-rw-r--r--kernel/entries.mli39
-rw-r--r--kernel/environ.mli126
-rw-r--r--kernel/esubst.mli33
-rw-r--r--kernel/indtypes.mli23
-rw-r--r--kernel/inductive.mli55
-rw-r--r--kernel/mod_subst.mli48
-rw-r--r--kernel/mod_typing.mli16
-rw-r--r--kernel/modops.mli20
-rw-r--r--kernel/names.mli68
-rw-r--r--kernel/pre_env.mli28
-rw-r--r--kernel/reduction.mli36
-rw-r--r--kernel/retroknowledge.mli42
-rw-r--r--kernel/safe_typing.mli46
-rw-r--r--kernel/sign.mli43
-rw-r--r--kernel/subtyping.mli16
-rw-r--r--kernel/term.mli336
-rw-r--r--kernel/term_typing.mli16
-rw-r--r--kernel/type_errors.mli22
-rw-r--r--kernel/typeops.mli52
-rw-r--r--kernel/univ.mli45
-rw-r--r--kernel/vconv.mli20
-rw-r--r--kernel/vm.mli29
29 files changed, 744 insertions, 765 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index f4dc0b14d..a8860d6d8 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -38,42 +38,43 @@ type instruction =
| Kpush
| Kpop of int
| Kpush_retaddr of Label.t
- | Kapply of int (* number of arguments *)
- | Kappterm of int * int (* number of arguments, slot size *)
- | Kreturn of int (* slot size *)
+ | Kapply of int (** number of arguments *)
+ | Kappterm of int * int (** number of arguments, slot size *)
+ | Kreturn of int (** slot size *)
| Kjump
| Krestart
- | Kgrab of int (* number of arguments *)
- | Kgrabrec of int (* rec arg *)
- | Kclosure of Label.t * int (* label, number of free variables *)
+ | Kgrab of int (** number of arguments *)
+ | Kgrabrec of int (** rec arg *)
+ | Kclosure of Label.t * int (** label, number of free variables *)
| Kclosurerec of int * int * Label.t array * Label.t array
- (* nb fv, init, lbl types, lbl bodies *)
+ (** nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
- (* nb fv, init, lbl types, lbl bodies *)
+ (** nb fv, init, lbl types, lbl bodies *)
| Kgetglobal of constant
| Kconst of structured_constant
- | Kmakeblock of int * tag (* size, tag *)
+ | Kmakeblock of int * tag (** size, tag *)
| Kmakeprod
| Kmakeswitchblock of Label.t * Label.t * annot_switch * int
- | Kswitch of Label.t array * Label.t array (* consts,blocks *)
+ | Kswitch of Label.t array * Label.t array (** consts,blocks *)
| Kpushfields of int
| Kfield of int
| Ksetfield of int
| Kstop
| Ksequence of bytecodes * bytecodes
-(* spiwack: instructions concerning integers *)
- | Kbranch of Label.t (* jump to label, is it needed ? *)
- | Kaddint31 (* adds the int31 in the accu
+
+(** spiwack: instructions concerning integers *)
+ | Kbranch of Label.t (** jump to label, is it needed ? *)
+ | Kaddint31 (** adds the int31 in the accu
and the one ontop of the stack *)
- | Kaddcint31 (* makes the sum and keeps the carry *)
- | Kaddcarrycint31 (* sum +1, keeps the carry *)
- | Ksubint31 (* subtraction modulo *)
- | Ksubcint31 (* subtraction, keeps the carry *)
- | Ksubcarrycint31 (* subtraction -1, keeps the carry *)
- | Kmulint31 (* multiplication modulo *)
- | Kmulcint31 (* multiplication, result in two
+ | Kaddcint31 (** makes the sum and keeps the carry *)
+ | Kaddcarrycint31 (** sum +1, keeps the carry *)
+ | Ksubint31 (** subtraction modulo *)
+ | Ksubcint31 (** subtraction, keeps the carry *)
+ | Ksubcarrycint31 (** subtraction -1, keeps the carry *)
+ | Kmulint31 (** multiplication modulo *)
+ | Kmulcint31 (** multiplication, result in two
int31, for exact computation *)
- | Kdiv21int31 (* divides a double size integer
+ | Kdiv21int31 (** divides a double size integer
(represented by an int31 in the
accumulator and one on the top of
the stack) by an int31. The result
@@ -81,23 +82,23 @@ type instruction =
rest.
If the divisor is 0, it returns
0. *)
- | Kdivint31 (* euclidian division (returns a pair
+ | Kdivint31 (** euclidian division (returns a pair
quotient,rest) *)
- | Kaddmuldivint31 (* generic operation for shifting and
+ | Kaddmuldivint31 (** generic operation for shifting and
cycling. Takes 3 int31 i j and s,
and returns x*2^s+y/(2^(31-s) *)
- | Kcompareint31 (* unsigned comparison of int31
+ | Kcompareint31 (** unsigned comparison of int31
cf COMPAREINT31 in
kernel/byterun/coq_interp.c
for more info *)
- | Khead0int31 (* Give the numbers of 0 in head of a in31*)
- | Ktail0int31 (* Give the numbers of 0 in tail of a in31
+ | Khead0int31 (** Give the numbers of 0 in head of a in31*)
+ | Ktail0int31 (** Give the numbers of 0 in tail of a in31
ie low bits *)
- | Kisconst of Label.t (* conditional jump *)
- | Kareconst of int*Label.t (* conditional jump *)
- | Kcompint31 (* dynamic compilation of int31 *)
- | Kdecompint31 (* dynamix decompilation of int31 *)
-(* /spiwack *)
+ | Kisconst of Label.t (** conditional jump *)
+ | Kareconst of int*Label.t (** conditional jump *)
+ | Kcompint31 (** dynamic compilation of int31 *)
+ | Kdecompint31 (** dynamix decompilation of int31
+ /spiwack *)
and bytecodes = instruction list
@@ -107,25 +108,25 @@ type fv_elem = FVnamed of identifier | FVrel of int
type fv = fv_elem array
-(* spiwack: this exception is expected to be raised by function expecting
+(** spiwack: this exception is expected to be raised by function expecting
closed terms. *)
exception NotClosed
(*spiwack: both type have been moved from Cbytegen because I needed then
for the retroknowledge *)
type vm_env = {
- size : int; (* longueur de la liste [n] *)
- fv_rev : fv_elem list (* [fvn; ... ;fv1] *)
+ size : int; (** longueur de la liste [n] *)
+ fv_rev : fv_elem list (** [fvn; ... ;fv1] *)
}
type comp_env = {
- nb_stack : int; (* nbre de variables sur la pile *)
- in_stack : int list; (* position dans la pile *)
- nb_rec : int; (* nbre de fonctions mutuellement *)
- (* recursives = nbr *)
- pos_rec : instruction list; (* instruction d'acces pour les variables *)
- (* de point fix ou de cofix *)
+ nb_stack : int; (** nbre de variables sur la pile *)
+ in_stack : int list; (** position dans la pile *)
+ nb_rec : int; (** nbre de fonctions mutuellement *)
+ (** recursives = nbr *)
+ pos_rec : instruction list; (** instruction d'acces pour les variables *)
+ (** de point fix ou de cofix *)
offset : int;
in_env : vm_env ref
}
@@ -140,7 +141,7 @@ type block =
| Bstrconst of structured_constant
| Bmakeblock of int * block array
| Bconstruct_app of int * int * int * block array
- (* tag , nparams, arity *)
+ (** tag , nparams, arity *)
| Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
- (* compilation function (see get_vm_constant_dynamic_info in
+ (** compilation function (see get_vm_constant_dynamic_info in
retroknowledge.mli for more info) , argument array *)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index f33fd6cb0..bf9c0be26 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -7,20 +7,20 @@ open Pre_env
val compile : env -> constr -> bytecodes * bytecodes * fv
- (* init, fun, fv *)
+ (** init, fun, fv *)
val compile_constant_body :
env -> constr_substituted option -> bool -> bool -> body_code
- (* opaque *) (* boxed *)
+ (** opaque *) (* boxed *)
-(* spiwack: this function contains the information needed to perform
+(** spiwack: this function contains the information needed to perform
the static compilation of int31 (trying and obtaining
a 31-bit integer in processor representation at compile time) *)
val compile_structured_int31 : bool -> constr array ->
structured_constant
-(* this function contains the information needed to perform
+(** this function contains the information needed to perform
the dynamic compilation of int31 (trying and obtaining a
31-bit integer in processor representation at runtime when
it failed at compile time *)
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 965228fa1..547155423 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -7,7 +7,8 @@ type reloc_info =
| Reloc_getglobal of constant
type patch = reloc_info * int
-(* A virer *)
+
+(** A virer *)
val subst_patch : Mod_subst.substitution -> patch -> patch
type emitcodes
@@ -37,4 +38,4 @@ val is_boxed : to_patch_substituted -> bool
val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted
val to_memory : bytecodes * bytecodes * fv -> to_patch
- (* init code, fun code, fv *)
+ (** init code, fun code, fv *)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 5cb6fc97c..ce339ab33 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -1,28 +1,27 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Pp
open Names
open Term
open Environ
open Esubst
-(*i*)
-(* Flags for profiling reductions. *)
+(** Flags for profiling reductions. *)
val stats : bool ref
val share : bool ref
val with_stats: 'a Lazy.t -> 'a
-(*s Delta implies all consts (both global (= by
+(** {6 Sect } *)
+(** Delta implies all consts (both global (= by
[kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
a LetIn expression is Letin reduction *)
@@ -32,12 +31,12 @@ val with_stats: 'a Lazy.t -> 'a
val all_opaque : transparent_state
val all_transparent : transparent_state
-(* Sets of reduction kinds. *)
+(** Sets of reduction kinds. *)
module type RedFlagsSig = sig
type reds
type red_kind
- (* The different kinds of reduction *)
+ (** The different kinds of reduction *)
val fBETA : red_kind
val fDELTA : red_kind
val fIOTA : red_kind
@@ -45,25 +44,25 @@ module type RedFlagsSig = sig
val fCONST : constant -> red_kind
val fVAR : identifier -> red_kind
- (* No reduction at all *)
+ (** No reduction at all *)
val no_red : reds
- (* Adds a reduction kind to a set *)
+ (** Adds a reduction kind to a set *)
val red_add : reds -> red_kind -> reds
- (* Removes a reduction kind to a set *)
+ (** Removes a reduction kind to a set *)
val red_sub : reds -> red_kind -> reds
- (* Adds a reduction kind to a set *)
+ (** Adds a reduction kind to a set *)
val red_add_transparent : reds -> transparent_state -> reds
- (* Build a reduction set from scratch = iter [red_add] on [no_red] *)
+ (** Build a reduction set from scratch = iter [red_add] on [no_red] *)
val mkflags : red_kind list -> reds
- (* Tests if a reduction kind is set *)
+ (** Tests if a reduction kind is set *)
val red_set : reds -> red_kind -> bool
- (* Gives the constant list *)
+ (** Gives the constant list *)
val red_get_const : reds -> bool * evaluable_global_reference list
end
@@ -89,19 +88,19 @@ val create: ('a infos -> constr -> 'a) -> reds -> env ->
(existential -> constr option) -> 'a infos
val evar_value : 'a infos -> existential -> constr option
-(************************************************************************)
-(*s Lazy reduction. *)
+(***********************************************************************
+ s Lazy reduction. *)
-(* [fconstr] is the type of frozen constr *)
+(** [fconstr] is the type of frozen constr *)
type fconstr
-(* [fconstr] can be accessed by using the function [fterm_of] and by
+(** [fconstr] can be accessed by using the function [fterm_of] and by
matching on type [fterm] *)
type fterm =
| FRel of int
- | FAtom of constr (* Metas and Sorts *)
+ | FAtom of constr (** Metas and Sorts *)
| FCast of fconstr * cast_kind * fconstr
| FFlex of table_key
| FInd of inductive
@@ -118,8 +117,8 @@ type fterm =
| FCLOS of constr * fconstr subs
| FLOCKED
-(************************************************************************)
-(*s A [stack] is a context of arguments, arguments are pushed by
+(***********************************************************************
+ s A [stack] is a context of arguments, arguments are pushed by
[append_stack] one array at a time but popped with [decomp_stack]
one by one *)
@@ -143,12 +142,13 @@ val stack_tail : int -> stack -> stack
val stack_nth : stack -> int -> fconstr
val zip_term : (fconstr -> constr) -> constr -> stack -> constr
-(* To lazy reduce a constr, create a [clos_infos] with
+(** To lazy reduce a constr, create a [clos_infos] with
[create_clos_infos], inject the term to reduce with [inject]; then use
a reduction function *)
val inject : constr -> fconstr
-(* mk_atom: prevents a term from being evaluated *)
+
+(** mk_atom: prevents a term from being evaluated *)
val mk_atom : constr -> fconstr
val fterm_of : fconstr -> fterm
@@ -156,33 +156,33 @@ val term_of_fconstr : fconstr -> constr
val destFLambda :
(fconstr subs -> constr -> fconstr) -> fconstr -> name * fconstr * fconstr
-(* Global and local constant cache *)
+(** Global and local constant cache *)
type clos_infos
val create_clos_infos :
?evars:(existential->constr option) -> reds -> env -> clos_infos
-(* Reduction function *)
+(** Reduction function *)
-(* [norm_val] is for strong normalization *)
+(** [norm_val] is for strong normalization *)
val norm_val : clos_infos -> fconstr -> constr
-(* [whd_val] is for weak head normalization *)
+(** [whd_val] is for weak head normalization *)
val whd_val : clos_infos -> fconstr -> constr
-(* [whd_stack] performs weak head normalization in a given stack. It
+(** [whd_stack] performs weak head normalization in a given stack. It
stops whenever a reduction is blocked. *)
val whd_stack :
clos_infos -> fconstr -> stack -> fconstr * stack
-(* Conversion auxiliary functions to do step by step normalisation *)
+(** Conversion auxiliary functions to do step by step normalisation *)
-(* [unfold_reference] unfolds references in a [fconstr] *)
+(** [unfold_reference] unfolds references in a [fconstr] *)
val unfold_reference : clos_infos -> table_key -> fconstr option
val eq_table_key : table_key -> table_key -> bool
-(************************************************************************)
-(*i This is for lazy debug *)
+(***********************************************************************
+ i This is for lazy debug *)
val lift_fconstr : int -> fconstr -> fconstr
val lift_fconstr_vect : int -> fconstr array -> fconstr array
@@ -200,4 +200,4 @@ val kl : clos_infos -> fconstr -> constr
val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
val optimise_closure : fconstr subs -> constr -> fconstr subs * constr
-(* End of cbn debug section i*)
+(** End of cbn debug section i*)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 86e108c6f..35e09072f 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -1,22 +1,22 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
open Names
-(* Order on section paths for unfolding.
+(** Order on section paths for unfolding.
If [oracle_order kn1 kn2] is true, then unfold kn1 first.
Note: the oracle does not introduce incompleteness, it only
tries to postpone unfolding of "opaque" constants. *)
val oracle_order : 'a tableKey -> 'a tableKey -> bool
-(* Priority for the expansion of constant in the conversion test.
+(** Priority for the expansion of constant in the conversion test.
* Higher levels means that the expansion is less prioritary.
* (And Expand stands for -oo, and Opaque +oo.)
* The default value (transparent constants) is [Level 0].
@@ -26,14 +26,14 @@ val transparent : level
val get_strategy : 'a tableKey -> level
-(* Sets the level of a constant.
+(** Sets the level of a constant.
* Level of RelKey constant cannot be set. *)
val set_strategy : 'a tableKey -> level -> unit
val get_transp_state : unit -> transparent_state
-(*****************************)
-(* Summary operations *)
+(****************************
+ Summary operations *)
type oracle
val init : unit -> unit
val freeze : unit -> oracle
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index db35031d9..5f30bce62 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -1,10 +1,10 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
@@ -14,7 +14,7 @@ open Declarations
open Environ
open Univ
-(*s Cooking the constants. *)
+(** {6 Cooking the constants. } *)
type work_list = identifier array Cmap.t * identifier array Mindmap.t
@@ -28,7 +28,7 @@ val cook_constant :
constr_substituted option * constant_type * constraints * bool * bool
* bool
-(*s Utility functions used in module [Discharge]. *)
+(** {6 Utility functions used in module [Discharge]. } *)
val expmod_constr : work_list -> constr -> constr
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 2fb2cb81c..c6cf8a751 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -1,30 +1,27 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Univ
open Term
open Cemitcodes
open Sign
open Mod_subst
-(*i*)
-(* This module defines the internal representation of global
+(** This module defines the internal representation of global
declarations. This includes global constants/axioms, mutual
inductive definitions, modules and module types *)
type engagement = ImpredicativeSet
-(**********************************************************************)
-(*s Representation of constants (Definition/Axiom) *)
+(** {6 Representation of constants (Definition/Axiom) } *)
type polymorphic_arity = {
poly_param_levels : universe option list;
@@ -41,7 +38,7 @@ val from_val : constr -> constr_substituted
val force : constr_substituted -> constr
type constant_body = {
- const_hyps : section_context; (* New: younger hyp at top *)
+ const_hyps : section_context; (** New: younger hyp at top *)
const_body : constr_substituted option;
const_type : constant_type;
const_body_code : to_patch_substituted;
@@ -52,8 +49,7 @@ type constant_body = {
val subst_const_body : substitution -> constant_body -> constant_body
-(**********************************************************************)
-(*s Representation of mutual inductive types in the kernel *)
+(** {6 Representation of mutual inductive types in the kernel } *)
type recarg =
| Norec
@@ -72,12 +68,12 @@ val recarg_length : wf_paths -> int -> int
val subst_wf_paths : substitution -> wf_paths -> wf_paths
-(*
-\begin{verbatim}
+(**
+{% \begin{verbatim} %}
Inductive I1 (params) : U1 := c11 : T11 | ... | c1p1 : T1p1
...
with In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
-\end{verbatim}
+{% \end{verbatim} %}
*)
type monomorphic_inductive_arity = {
@@ -90,94 +86,72 @@ type inductive_arity =
| Polymorphic of polymorphic_arity
type one_inductive_body = {
+(** {8 Primitive datas } *)
-(* Primitive datas *)
+ mind_typename : identifier; (** Name of the type: [Ii] *)
- (* Name of the type: [Ii] *)
- mind_typename : identifier;
+ mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
- (* Arity context of [Ii] with parameters: [forall params, Ui] *)
- mind_arity_ctxt : rel_context;
+ mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *)
- (* Arity sort and original user arity if monomorphic *)
- mind_arity : inductive_arity;
+ mind_consnames : identifier array; (** Names of the constructors: [cij] *)
- (* Names of the constructors: [cij] *)
- mind_consnames : identifier array;
-
- (* Types of the constructors with parameters: [forall params, Tij],
- where the Ik are replaced by de Bruijn index in the context
- I1:forall params, U1 .. In:forall params, Un *)
mind_user_lc : types array;
+ (** Types of the constructors with parameters: [forall params, Tij],
+ where the Ik are replaced by de Bruijn index in the
+ context I1:forall params, U1 .. In:forall params, Un *)
-(* Derived datas *)
+(** {8 Derived datas } *)
- (* Number of expected real arguments of the type (no let, no params) *)
- mind_nrealargs : int;
+ mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *)
- (* Length of realargs context (with let, no params) *)
- mind_nrealargs_ctxt : int;
+ mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *)
- (* List of allowed elimination sorts *)
- mind_kelim : sorts_family list;
+ mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
- (* Head normalized constructor types so that their conclusion is atomic *)
- mind_nf_lc : types array;
+ mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *)
- (* Length of the signature of the constructors (with let, w/o params)
- (not to be used in the kernel!) *)
mind_consnrealdecls : int array;
+ (** Length of the signature of the constructors (with let, w/o params)
+ (not used in the kernel) *)
- (* Signature of recursive arguments in the constructors *)
- mind_recargs : wf_paths;
+ mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
-(* Datas for bytecode compilation *)
+(** {8 Datas for bytecode compilation } *)
- (* number of constant constructor *)
- mind_nb_constant : int;
+ mind_nb_constant : int; (** number of constant constructor *)
- (* number of no constant constructor *)
- mind_nb_args : int;
+ mind_nb_args : int; (** number of no constant constructor *)
mind_reloc_tbl : Cbytecodes.reloc_table;
}
type mutual_inductive_body = {
- (* The component of the mutual inductive block *)
- mind_packets : one_inductive_body array;
+ mind_packets : one_inductive_body array; (** The component of the mutual inductive block *)
- (* Whether the inductive type has been declared as a record *)
- mind_record : bool;
+ mind_record : bool; (** Whether the inductive type has been declared as a record *)
- (* Whether the type is inductive or coinductive *)
- mind_finite : bool;
+ mind_finite : bool; (** Whether the type is inductive or coinductive *)
- (* Number of types in the block *)
- mind_ntypes : int;
+ mind_ntypes : int; (** Number of types in the block *)
- (* Section hypotheses on which the block depends *)
- mind_hyps : section_context;
+ mind_hyps : section_context; (** Section hypotheses on which the block depends *)
- (* Number of expected parameters *)
- mind_nparams : int;
+ mind_nparams : int; (** Number of expected parameters *)
- (* Number of recursively uniform (i.e. ordinary) parameters *)
- mind_nparams_rec : int;
+ mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *)
- (* The context of parameters (includes let-in declaration) *)
- mind_params_ctxt : rel_context;
+ mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *)
- (* Universes constraints enforced by the inductive declaration *)
- mind_constraints : constraints;
+ mind_constraints : constraints; (** Universes constraints enforced by the inductive declaration *)
}
val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
-(**********************************************************************)
-(*s Modules: signature component specifications, module types, and
- module declarations *)
+(** {6 Modules: signature component specifications, module types, and
+ module declarations } *)
type structure_field_body =
| SFBconst of constant_body
@@ -199,29 +173,29 @@ and with_declaration_body =
| With_definition_body of identifier list * constant_body
and module_body =
- { (*absolute path of the module*)
+ { (** absolute path of the module *)
mod_mp : module_path;
- (* Implementation *)
+ (** Implementation *)
mod_expr : struct_expr_body option;
- (* Signature *)
+ (** Signature *)
mod_type : struct_expr_body;
- (* algebraic structure expression is kept
+ (** algebraic structure expression is kept
if it's relevant for extraction *)
mod_type_alg : struct_expr_body option;
- (* set of all constraint in the module *)
+ (** set of all constraint in the module *)
mod_constraints : constraints;
- (* quotiented set of equivalent constant and inductive name *)
+ (** quotiented set of equivalent constant and inductive name *)
mod_delta : delta_resolver;
mod_retroknowledge : Retroknowledge.action list}
and module_type_body =
{
- (*Path of the module type*)
+ (** Path of the module type *)
typ_mp : module_path;
typ_expr : struct_expr_body;
- (* algebraic structure expression is kept
+ (** algebraic structure expression is kept
if it's relevant for extraction *)
typ_expr_alg : struct_expr_body option ;
typ_constraints : constraints;
- (* quotiented set of equivalent constant and inductive name *)
+ (** quotiented set of equivalent constant and inductive name *)
typ_delta :delta_resolver}
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 20fbbb8e7..2cfdf9314 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -1,43 +1,40 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Univ
open Term
open Sign
-(*i*)
-(* This module defines the entry types for global declarations. This
+(** This module defines the entry types for global declarations. This
information is entered in the environments. This includes global
constants/axioms, mutual inductive definitions, modules and module
types *)
-(*s Local entries *)
+(** {6 Local entries } *)
type local_entry =
| LocalDef of constr
| LocalAssum of constr
-(*s Declaration of inductive types. *)
+(** {6 Declaration of inductive types. } *)
-(* Assume the following definition in concrete syntax:
-\begin{verbatim}
-Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
+(** Assume the following definition in concrete syntax:
+{v Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
...
-with Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
-\end{verbatim}
-then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
-[mind_entry_arity] is [Ai], defined in context [[[x1:X1;...;xn:Xn]];
+with Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp. v}
+
+then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
+[mind_entry_arity] is [Ai], defined in context [x1:X1;...;xn:Xn];
[mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
*)
@@ -53,7 +50,7 @@ type mutual_inductive_entry = {
mind_entry_params : (identifier * local_entry) list;
mind_entry_inds : one_inductive_entry list }
-(*s Constants (Definition/Axiom) *)
+(** {6 Constants (Definition/Axiom) } *)
type definition_entry = {
const_entry_body : constr;
@@ -67,7 +64,7 @@ type constant_entry =
| DefinitionEntry of definition_entry
| ParameterEntry of parameter_entry
-(*s Modules *)
+(** {6 Modules } *)
type specification_entry =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 667a0ed43..fce149e10 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -1,26 +1,24 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Term
open Declarations
open Sign
-(*i*)
-(*s Unsafe environments. We define here a datatype for environments.
+(** Unsafe environments. We define here a datatype for environments.
Since typing is not yet defined, it is not possible to check the
informations added in environments, and that is why we speak here
of ``unsafe'' environments. *)
-(* Environments have the following components:
+(** Environments have the following components:
- a context for de Bruijn variables
- a context for de Bruijn variables vm values
- a context for section variables and goal assumptions
@@ -50,27 +48,27 @@ val named_context_val : env -> named_context_val
val engagement : env -> engagement option
-(* is the local context empty *)
+(** is the local context empty *)
val empty_context : env -> bool
-(************************************************************************)
-(*s Context of de Bruijn variables ([rel_context]) *)
+(** {5 Context of de Bruijn variables ([rel_context]) } *)
+
val nb_rel : env -> int
val push_rel : rel_declaration -> env -> env
val push_rel_context : rel_context -> env -> env
val push_rec_types : rec_declaration -> env -> env
-(* Looks up in the context of local vars referred by indice ([rel_context]) *)
-(* raises [Not_found] if the index points out of the context *)
+(** Looks up in the context of local vars referred by indice ([rel_context])
+ raises [Not_found] if the index points out of the context *)
val lookup_rel : int -> env -> rel_declaration
val evaluable_rel : int -> env -> bool
-(*s Recurrence on [rel_context] *)
+(** {6 Recurrence on [rel_context] } *)
+
val fold_rel_context :
(env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
-(************************************************************************)
-(* Context of variables (section variables and goal assumptions) *)
+(** {5 Context of variables (section variables and goal assumptions) } *)
val named_context_of_val : named_context_val -> named_context
val named_vals_of_val : named_context_val -> Pre_env.named_vals
@@ -78,7 +76,7 @@ val val_of_named_context : named_context -> named_context_val
val empty_named_context_val : named_context_val
-(* [map_named_val f ctxt] apply [f] to the body and the type of
+(** [map_named_val f ctxt] apply [f] to the body and the type of
each declarations.
*** /!\ *** [f t] should be convertible with t *)
val map_named_val :
@@ -90,8 +88,8 @@ val push_named_context_val :
-(* Looks up in the context of local vars referred by names ([named_context]) *)
-(* raises [Not_found] if the identifier is not found *)
+(** Looks up in the context of local vars referred by names ([named_context])
+ raises [Not_found] if the identifier is not found *)
val lookup_named : variable -> env -> named_declaration
val lookup_named_val : variable -> named_context_val -> named_declaration
@@ -99,34 +97,36 @@ val evaluable_named : variable -> env -> bool
val named_type : variable -> env -> types
val named_body : variable -> env -> constr option
-(*s Recurrence on [named_context]: older declarations processed first *)
+(** {6 Recurrence on [named_context]: older declarations processed first } *)
val fold_named_context :
(env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
-(* Recurrence on [named_context] starting from younger decl *)
+(** Recurrence on [named_context] starting from younger decl *)
val fold_named_context_reverse :
('a -> named_declaration -> 'a) -> init:'a -> env -> 'a
-(* This forgets named and rel contexts *)
+(** This forgets named and rel contexts *)
val reset_context : env -> env
-(* This forgets rel context and sets a new named context *)
+
+(** This forgets rel context and sets a new named context *)
val reset_with_named_context : named_context_val -> env -> env
-(************************************************************************)
-(*s Global constants *)
-(*s Add entries to global environment *)
-val add_constant : constant -> constant_body -> env -> env
+(** {5 Global constants }
+ {6 Add entries to global environment } *)
-(* Looks up in the context of global constant names *)
-(* raises [Not_found] if the required path is not found *)
+val add_constant : constant -> constant_body -> env -> env
+(** Looks up in the context of global constant names
+ raises [Not_found] if the required path is not found *)
val lookup_constant : constant -> env -> constant_body
val evaluable_constant : constant -> env -> bool
-(*s [constant_value env c] raises [NotEvaluableConst Opaque] if
+(** {6 Sect } *)
+(** [constant_value env c] raises [NotEvaluableConst Opaque] if
[c] is opaque and [NotEvaluableConst NoBody] if it has no
body and [Not_found] if it does not exist in [env] *)
+
type const_evaluation_result = NoBody | Opaque
exception NotEvaluableConst of const_evaluation_result
@@ -134,44 +134,45 @@ val constant_value : env -> constant -> constr
val constant_type : env -> constant -> constant_type
val constant_opt_value : env -> constant -> constr option
-(************************************************************************)
-(*s Inductive types *)
+(** {5 Inductive types } *)
+
val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
-(* Looks up in the context of global inductive names *)
-(* raises [Not_found] if the required path is not found *)
+(** Looks up in the context of global inductive names
+ raises [Not_found] if the required path is not found *)
val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
-(************************************************************************)
-(*s Modules *)
+(** {5 Modules } *)
+
val add_modtype : module_path -> module_type_body -> env -> env
-(* [shallow_add_module] does not add module components *)
+(** [shallow_add_module] does not add module components *)
val shallow_add_module : module_path -> module_body -> env -> env
val lookup_module : module_path -> env -> module_body
val lookup_modtype : module_path -> env -> module_type_body
-(************************************************************************)
-(*s Universe constraints *)
+(** {5 Universe constraints } *)
+
val set_universes : Univ.universes -> env -> env
val add_constraints : Univ.constraints -> env -> env
val set_engagement : engagement -> env -> env
-(************************************************************************)
-(* Sets of referred section variables *)
-(* [global_vars_set env c] returns the list of [id]'s occurring either
+(** {6 Sets of referred section variables }
+ [global_vars_set env c] returns the list of [id]'s occurring either
directly as [Var id] in [c] or indirectly as a section variable
dependent in a global reference occurring in [c] *)
+
val global_vars_set : env -> constr -> Idset.t
-(* the constr must be a global reference *)
+
+(** the constr must be a global reference *)
val vars_of_global : env -> constr -> identifier list
val keep_hyps : env -> Idset.t -> section_context
-(************************************************************************)
-(*s Unsafe judgments. We introduce here the pre-type of judgments, which is
+(** {5 Unsafe judgments. }
+ We introduce here the pre-type of judgments, which is
actually only a datatype to store a term with its type and the type of its
type. *)
@@ -188,23 +189,22 @@ type unsafe_type_judgment = {
utj_type : sorts }
-(*s Compilation of global declaration *)
+(** {6 Compilation of global declaration } *)
val compile_constant_body :
env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code
- (* opaque *) (* boxed *)
+ (** opaque *) (* boxed *)
exception Hyp_not_found
-(* [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and
+(** [apply_to_hyp sign id f] split [sign] into [tail::(id,_,_)::head] and
return [tail::(f head (id,_,_) (rev tail))::head].
the value associated to id should not change *)
-
val apply_to_hyp : named_context_val -> variable ->
(named_context -> named_declaration -> named_context -> named_declaration) ->
named_context_val
-(* [apply_to_hyp_and_dependent_on sign id f g] split [sign] into
+(** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into
[tail::(id,_,_)::head] and
return [(g tail)::(f (id,_,_))::head]. *)
val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
@@ -219,9 +219,10 @@ val insert_after_hyp : named_context_val -> variable ->
val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
-(* spiwack: functions manipulating the retroknowledge *)
-open Retroknowledge
+open Retroknowledge
+(** functions manipulating the retroknowledge
+ @author spiwack *)
val retroknowledge : (retroknowledge->'a) -> env -> 'a
val registered : env -> field -> bool
@@ -232,19 +233,18 @@ val register : env -> field -> Retroknowledge.entry -> env
-(******************************************************************)
-(* spiwack: a few declarations for the "Print Assumption" command *)
-
+(** a few declarations for the "Print Assumption" command
+ @author spiwack *)
type context_object =
- | Variable of identifier (* A section variable or a Let definition *)
- | Axiom of constant (* An axiom or a constant. *)
- | Opaque of constant (* An opaque constant. *)
+ | Variable of identifier (** A section variable or a Let definition *)
+ | Axiom of constant (** An axiom or a constant. *)
+ | Opaque of constant (** An opaque constant. *)
-(* AssumptionSet.t is a set of [assumption] *)
+(** AssumptionSet.t is a set of [assumption] *)
module OrderedContextObject : Set.OrderedType with type t = context_object
module ContextObjectMap : Map.S with type key = context_object
-(* collects all the assumptions (optionally including opaque definitions)
+(** collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type) *)
val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index bf1d23241..bbb3d838e 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -1,15 +1,16 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*s Explicit substitutions of type ['a]. *)
-(* - ESID(n) = %n END bounded identity
+(** {6 Sect } *)
+(** Explicit substitutions of type ['a].
+ - ESID(n) = %n END bounded identity
* - CONS([|t1..tn|],S) = (S.t1...tn) parallel substitution
* (beware of the order: indice 1 is substituted by tn)
* - SHIFT(n,S) = (^n o S) terms in S are relocated with n vars
@@ -21,15 +22,16 @@ type 'a subs =
| SHIFT of int * 'a subs
| LIFT of int * 'a subs
-(* Derived constructors granting basic invariants *)
+(** Derived constructors granting basic invariants *)
val subs_cons: 'a array * 'a subs -> 'a subs
val subs_shft: int * 'a subs -> 'a subs
val subs_lift: 'a subs -> 'a subs
val subs_liftn: int -> 'a subs -> 'a subs
-(* [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *)
+
+(** [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *)
val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
-(* [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
+(** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
* [subs]. The result is either (Inl(lams,v)) when the variable is
* substituted by value [v] under lams binders (i.e. v *has* to be
* shifted by lams), or (Inr (k',p)) when the variable k is just relocated
@@ -38,17 +40,18 @@ val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
*)
val expand_rel: int -> 'a subs -> (int * 'a, int * int option) Util.union
-(* Tests whether a substitution behaves like the identity *)
+(** Tests whether a substitution behaves like the identity *)
val is_subs_id: 'a subs -> bool
-(* Composition of substitutions: [comp mk_clos s1 s2] computes a
+(** Composition of substitutions: [comp mk_clos s1 s2] computes a
* substitution equivalent to applying s2 then s1. Argument
* mk_clos is used when a closure has to be created, i.e. when
* s1 is applied on an element of s2.
*)
val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
-(*s Compact representation of explicit relocations. \\
+(** {6 Sect } *)
+(** Compact representation of explicit relocations. \\
[ELSHFT(l,n)] == lift of [n], then apply [lift l].
[ELLFT(n,l)] == apply [l] to de Bruijn > [n] i.e under n binders. *)
type lift =
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 0cbe15034..c29e5475d 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Univ
open Term
@@ -16,13 +15,13 @@ open Declarations
open Environ
open Entries
open Typeops
-(*i*)
-(*s The different kinds of errors that may result of a malformed inductive
+(** {6 Sect } *)
+(** The different kinds of errors that may result of a malformed inductive
definition. *)
-(* Errors related to inductive constructions *)
+(** Errors related to inductive constructions *)
type inductive_error =
| NonPos of env * constr * constr
| NotEnoughArgs of env * constr * constr
@@ -37,7 +36,7 @@ type inductive_error =
exception InductiveError of inductive_error
-(*s The following function does checks on inductive declarations. *)
+(** {6 The following function does checks on inductive declarations. } *)
val check_inductive :
env -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 8fe8eb11f..7f2b08844 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,24 +1,22 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Univ
open Term
open Declarations
open Environ
-(*i*)
-(*s Extracting an inductive type from a construction *)
+(** {6 Extracting an inductive type from a construction } *)
-(* [find_m*type env sigma c] coerce [c] to an recursive type (I args).
+(** [find_m*type env sigma c] coerce [c] to an recursive type (I args).
[find_rectype], [find_inductive] and [find_coinductive]
respectively accepts any recursive type, only an inductive type and
only a coinductive type.
@@ -30,31 +28,32 @@ val find_coinductive : env -> types -> inductive * constr list
type mind_specif = mutual_inductive_body * one_inductive_body
-(*s Fetching information in the environment about an inductive type.
+(** {6 Sect } *)
+(** Fetching information in the environment about an inductive type.
Raises [Not_found] if the inductive type is not found. *)
val lookup_mind_specif : env -> inductive -> mind_specif
-(*s Functions to build standard types related to inductive *)
+(** {6 Functions to build standard types related to inductive } *)
val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list
val type_of_inductive : env -> mind_specif -> types
val elim_sorts : mind_specif -> sorts_family list
-(* Return type as quoted by the user *)
+(** Return type as quoted by the user *)
val type_of_constructor : constructor -> mind_specif -> types
-(* Return constructor types in normal form *)
+(** Return constructor types in normal form *)
val arities_of_constructors : inductive -> mind_specif -> types array
-(* Return constructor types in user form *)
+(** Return constructor types in user form *)
val type_of_constructors : inductive -> mind_specif -> types array
-(* Transforms inductive specification into types (in nf) *)
+(** Transforms inductive specification into types (in nf) *)
val arities_of_specif : mutual_inductive -> mind_specif -> types array
-(* [type_case_branches env (I,args) (p:A) c] computes useful types
+(** [type_case_branches env (I,args) (p:A) c] computes useful types
about the following Cases expression:
<p>Cases (c :: (I args)) of b1..bn end
It computes the type of every branch (pattern variables are
@@ -69,20 +68,20 @@ val build_branches_type :
inductive -> mutual_inductive_body * one_inductive_body ->
constr list -> constr -> types array
-(* Return the arity of an inductive type *)
+(** Return the arity of an inductive type *)
val mind_arity : one_inductive_body -> rel_context * sorts_family
val inductive_sort_family : one_inductive_body -> sorts_family
-(* Check a [case_info] actually correspond to a Case expression on the
+(** Check a [case_info] actually correspond to a Case expression on the
given inductive type. *)
val check_case_info : env -> inductive -> case_info -> unit
-(*s Guard conditions for fix and cofix-points. *)
+(** {6 Guard conditions for fix and cofix-points. } *)
val check_fix : env -> fixpoint -> unit
val check_cofix : env -> cofixpoint -> unit
-(*s Support for sort-polymorphic inductive types *)
+(** {6 Support for sort-polymorphic inductive types } *)
val type_of_inductive_knowing_parameters :
env -> one_inductive_body -> types array -> types
@@ -92,8 +91,8 @@ val max_inductive_sort : sorts array -> universe
val instantiate_universes : env -> rel_context ->
polymorphic_arity -> types array -> rel_context * sorts
-(***************************************************************)
-(* Debug *)
+(**************************************************************
+ Debug *)
type size = Large | Strict
type subterm_spec =
@@ -102,13 +101,13 @@ type subterm_spec =
| Not_subterm
type guard_env =
{ env : env;
- (* dB of last fixpoint *)
+ (** dB of last fixpoint *)
rel_min : int;
- (* inductive of recarg of each fixpoint *)
+ (** inductive of recarg of each fixpoint *)
inds : inductive array;
- (* the recarg information of inductive family *)
+ (** the recarg information of inductive family *)
recvec : wf_paths array;
- (* dB of variables denoting subterms *)
+ (** dB of variables denoting subterms *)
genv : subterm_spec Lazy.t list;
}
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index a948d1647..53925955e 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -1,19 +1,19 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*s [Mod_subst] *)
+(** {6 [Mod_subst] } *)
open Names
open Term
-(* A delta_resolver maps name (constant, inductive, module_path)
+(** A delta_resolver maps name (constant, inductive, module_path)
to canonical name *)
type delta_resolver
@@ -35,30 +35,30 @@ val add_mp_delta_resolver : module_path -> module_path -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
-(* Apply the substitution on the domain of the resolver *)
+(** Apply the substitution on the domain of the resolver *)
val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
-(* Apply the substitution on the codomain of the resolver *)
+(** Apply the substitution on the codomain of the resolver *)
val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
val subst_dom_codom_delta_resolver :
substitution -> delta_resolver -> delta_resolver
-(* *_of_delta return the associated name of arg2 in arg1 *)
+(** *_of_delta return the associated name of arg2 in arg1 *)
val constant_of_delta : delta_resolver -> constant -> constant
val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
val delta_of_mp : delta_resolver -> module_path -> module_path
-(* Extract the set of inlined constant in the resolver *)
+(** Extract the set of inlined constant in the resolver *)
val inline_of_delta : delta_resolver -> kernel_name list
-(* remove_mp is used for the computation of a resolver induced by Include P *)
+(** remove_mp is used for the computation of a resolver induced by Include P *)
val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver
-(* mem tests *)
+(** mem tests *)
val mp_in_delta : module_path -> delta_resolver -> bool
val con_in_delta : constant -> delta_resolver -> bool
@@ -69,20 +69,20 @@ val mind_in_delta : mutual_inductive -> delta_resolver -> bool
val empty_subst : substitution
-(* add_* add [arg2/arg1]{arg3} to the substitution with no
+(** add_* add [arg2/arg1]\{arg3\} to the substitution with no
sequential composition *)
val add_mbid :
mod_bound_id -> module_path -> delta_resolver -> substitution -> substitution
val add_mp :
module_path -> module_path -> delta_resolver -> substitution -> substitution
-(* map_* create a new substitution [arg2/arg1]{arg3} *)
+(** map_* create a new substitution [arg2/arg1]\{arg3\} *)
val map_mbid :
mod_bound_id -> module_path -> delta_resolver -> substitution
val map_mp :
module_path -> module_path -> delta_resolver -> substitution
-(* sequential composition:
+(** sequential composition:
[substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
*)
val join : substitution -> substitution -> substitution
@@ -97,9 +97,9 @@ val debug_string_of_subst : substitution -> string
val debug_pr_subst : substitution -> Pp.std_ppcmds
val debug_string_of_delta : delta_resolver -> string
val debug_pr_delta : delta_resolver -> Pp.std_ppcmds
-(*i*)
+(**/**)
-(* [subst_mp sub mp] guarantees that whenever the result of the
+(** [subst_mp sub mp] guarantees that whenever the result of the
substitution is structutally equal [mp], it is equal by pointers
as well [==] *)
@@ -115,7 +115,7 @@ val subst_kn :
val subst_con :
substitution -> constant -> constant * constr
-(* Here the semantics is completely unclear.
+(** Here the semantics is completely unclear.
What does "Hint Unfold t" means when "t" is a parameter?
Does the user mean "Unfold X.t" or does she mean "Unfold y"
where X.t is later on instantiated with y? I choose the first
@@ -123,14 +123,14 @@ val subst_con :
val subst_evaluable_reference :
substitution -> evaluable_global_reference -> evaluable_global_reference
-(* [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
+(** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name
-(* [subst_mps sub c] performs the substitution [sub] on all kernel
+(** [subst_mps sub c] performs the substitution [sub] on all kernel
names appearing in [c] *)
val subst_mps : substitution -> constr -> constr
-(* [occur_*id id sub] returns true iff [id] occurs in [sub]
+(** [occur_*id id sub] returns true iff [id] occurs in [sub]
on either side *)
val occur_mbid : mod_bound_id -> substitution -> bool
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 63f7696c4..188e4809c 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Declarations
open Environ
open Entries
open Mod_subst
open Names
-(*i*)
val translate_module : env -> module_path -> bool -> module_entry
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 3488a312f..0c61e773b 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Util
open Names
open Univ
@@ -16,9 +15,8 @@ open Environ
open Declarations
open Entries
open Mod_subst
-(*i*)
-(* Various operations on modules and module types *)
+(** Various operations on modules and module types *)
val module_body_of_type : module_path -> module_type_body -> module_body
@@ -36,7 +34,7 @@ val subst_signature : substitution -> structure_body -> structure_body
val add_signature :
module_path -> structure_body -> delta_resolver -> env -> env
-(* adds a module and its components, but not the constraints *)
+(** adds a module and its components, but not the constraints *)
val add_module : module_body -> env -> env
val check_modpath_equiv : env -> module_path -> module_path -> unit
diff --git a/kernel/names.mli b/kernel/names.mli
index e4d2c9322..f712c8d19 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -1,51 +1,53 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*s Identifiers *)
+(** {6 Identifiers } *)
type identifier
type name = Name of identifier | Anonymous
-(* Parsing and printing of identifiers *)
+
+(** Parsing and printing of identifiers *)
val string_of_id : identifier -> string
val id_of_string : string -> identifier
val id_ord : identifier -> identifier -> int
-(* Identifiers sets and maps *)
+(** Identifiers sets and maps *)
module Idset : Set.S with type elt = identifier
module Idpred : Predicate.S with type elt = identifier
module Idmap : Map.S with type key = identifier
-(*s Directory paths = section names paths *)
+(** {6 Directory paths = section names paths } *)
type module_ident = identifier
module ModIdmap : Map.S with type key = module_ident
type dir_path
-(* Inner modules idents on top of list (to improve sharing).
+(** Inner modules idents on top of list (to improve sharing).
For instance: A.B.C is ["C";"B";"A"] *)
val make_dirpath : module_ident list -> dir_path
val repr_dirpath : dir_path -> module_ident list
val empty_dirpath : dir_path
-(* Printing of directory paths as ["coq_root.module.submodule"] *)
+(** Printing of directory paths as ["coq_root.module.submodule"] *)
val string_of_dirpath : dir_path -> string
-(*s Unique identifier to be used as "self" in structures and
+(** {6 Sect } *)
+(** Unique identifier to be used as "self" in structures and
signatures - invisible for users *)
type label
type mod_self_id
-(* The first argument is a file name - to prevent conflict between
+(** The first argument is a file name - to prevent conflict between
different files *)
val make_msid : dir_path -> string -> mod_self_id
val repr_msid : mod_self_id -> int * string * dir_path
@@ -55,7 +57,7 @@ val refresh_msid : mod_self_id -> mod_self_id
val debug_string_of_msid : mod_self_id -> string
val string_of_msid : mod_self_id -> string
-(*s Unique names for bound modules *)
+(** {6 Unique names for bound modules } *)
type mod_bound_id
val make_mbid : dir_path -> string -> mod_bound_id
@@ -65,7 +67,7 @@ val label_of_mbid : mod_bound_id -> label
val debug_string_of_mbid : mod_bound_id -> string
val string_of_mbid : mod_bound_id -> string
-(*s Names of structure elements *)
+(** {6 Names of structure elements } *)
val mk_label : string -> label
val string_of_label : label -> string
@@ -76,11 +78,11 @@ val id_of_label : label -> identifier
module Labset : Set.S with type elt = label
module Labmap : Map.S with type key = label
-(*s The module part of the kernel name *)
+(** {6 The module part of the kernel name } *)
type module_path =
| MPfile of dir_path
| MPbound of mod_bound_id
- (* | MPapp of module_path * module_path very soon *)
+ (** | MPapp of module_path * module_path very soon *)
| MPdot of module_path * label
@@ -91,18 +93,18 @@ val string_of_mp : module_path -> string
module MPset : Set.S with type elt = module_path
module MPmap : Map.S with type key = module_path
-(* Name of the toplevel structure *)
+(** Name of the toplevel structure *)
val initial_msid : mod_self_id
-val initial_path : module_path (* [= MPself initial_msid] *)
+val initial_path : module_path (** [= MPself initial_msid] *)
-(* Initial "seed" of the unique identifier generator *)
+(** Initial "seed" of the unique identifier generator *)
val initial_dir : dir_path
-(*s The absolute names of objects seen by kernel *)
+(** {6 The absolute names of objects seen by kernel } *)
type kernel_name
-(* Constructor and destructor *)
+(** Constructor and destructor *)
val make_kn : module_path -> dir_path -> label -> kernel_name
val repr_kn : kernel_name -> module_path * dir_path * label
@@ -118,17 +120,19 @@ module KNpred : Predicate.S with type elt = kernel_name
module KNmap : Map.S with type key = kernel_name
-(*s Specific paths for declarations *)
+(** {6 Specific paths for declarations } *)
type variable = identifier
type constant
type mutual_inductive
-(* Beware: first inductive has index 0 *)
+
+(** Beware: first inductive has index 0 *)
type inductive = mutual_inductive * int
-(* Beware: first constructor has index 1 *)
+
+(** Beware: first constructor has index 1 *)
type constructor = inductive * int
-(* *_env modules consider an order on user part of names
+(** *_env modules consider an order on user part of names
the others consider an order on canonical part of names*)
module Cmap : Map.S with type key = constant
module Cmap_env : Map.S with type key = constant
@@ -191,7 +195,7 @@ val index_of_constructor : constructor -> int
val eq_ind : inductive -> inductive -> bool
val eq_constructor : constructor -> constructor -> bool
-(* Better to have it here that in Closure, since required in grammar.cma *)
+(** Better to have it here that in Closure, since required in grammar.cma *)
type evaluable_global_reference =
| EvalVarRef of identifier
| EvalConstRef of constant
@@ -199,7 +203,7 @@ type evaluable_global_reference =
val eq_egr : evaluable_global_reference -> evaluable_global_reference
-> bool
-(* Hash-consing *)
+(** Hash-consing *)
val hcons_names : unit ->
(constant -> constant) *
(mutual_inductive -> mutual_inductive) * (dir_path -> dir_path) *
@@ -220,8 +224,8 @@ val full_transparent_state : transparent_state
val var_full_transparent_state : transparent_state
val cst_full_transparent_state : transparent_state
-type inv_rel_key = int (* index in the [rel_context] part of environment
- starting by the end, {\em inverse}
+type inv_rel_key = int (** index in the [rel_context] part of environment
+ starting by the end, {e inverse}
of de Bruijn indice *)
type id_key = inv_rel_key tableKey
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 718132b32..619c1afcb 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -1,12 +1,12 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
-(* $Id$ *)
+(** {% $ %}Id: pre_env.mli 12406 2009-10-21 15:12:52Z soubiran {% $ %} *)
open Util
open Names
@@ -15,7 +15,7 @@ open Univ
open Term
open Declarations
-(* The type of environments. *)
+(** The type of environments. *)
type key = int option ref
@@ -57,25 +57,27 @@ val empty_named_context_val : named_context_val
val empty_env : env
-(* Rel context *)
+(** Rel context *)
val nb_rel : env -> int
val push_rel : rel_declaration -> env -> env
val lookup_rel_val : int -> env -> lazy_val
val env_of_rel : int -> env -> env
-(* Named context *)
+
+(** Named context *)
val push_named_context_val :
named_declaration -> named_context_val -> named_context_val
val push_named : named_declaration -> env -> env
val lookup_named_val : identifier -> env -> lazy_val
val env_of_named : identifier -> env -> env
-(* Global constants *)
+
+(** Global constants *)
val lookup_constant_key : constant -> env -> constant_key
val lookup_constant : constant -> env -> constant_body
-(* Mutual Inductives *)
+(** Mutual Inductives *)
val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index f2c9df156..06d4478b2 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -1,21 +1,19 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Term
open Environ
open Closure
-(*i*)
-(************************************************************************)
-(*s Reduction functions *)
+(***********************************************************************
+ s Reduction functions *)
val whd_betaiotazeta : constr -> constr
val whd_betadeltaiota : env -> constr -> constr
@@ -23,8 +21,8 @@ val whd_betadeltaiota_nolet : env -> constr -> constr
val nf_betaiota : constr -> constr
-(************************************************************************)
-(*s conversion functions *)
+(***********************************************************************
+ s conversion functions *)
exception NotConvertible
exception NotConvertibleVect of int
@@ -53,7 +51,7 @@ val conv_leq :
val conv_leq_vecti :
?evars:(existential->constr option) -> types array conversion_function
-(* option for conversion *)
+(** option for conversion *)
val set_vm_conv : (conv_pb -> types conversion_function) -> unit
val vm_conv : conv_pb -> types conversion_function
@@ -63,18 +61,18 @@ val default_conv_leq : types conversion_function
(************************************************************************)
-(* Builds an application node, reducing beta redexes it may produce. *)
+(** Builds an application node, reducing beta redexes it may produce. *)
val beta_appvect : constr -> constr array -> constr
-(* Builds an application node, reducing the [n] first beta-zeta redexes. *)
+(** Builds an application node, reducing the [n] first beta-zeta redexes. *)
val betazeta_appvect : int -> constr -> constr array -> constr
-(* Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *)
+(** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *)
val hnf_prod_applist : env -> types -> constr list -> types
-(************************************************************************)
-(*s Recognizing products and arities modulo reduction *)
+(***********************************************************************
+ s Recognizing products and arities modulo reduction *)
val dest_prod : env -> types -> rel_context * types
val dest_prod_assum : env -> types -> rel_context * types
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 0f1cdc8e2..19f30cd8f 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -1,24 +1,22 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Term
-(*i*)
type retroknowledge
-(* aliased type for clarity purpose*)
+(** aliased type for clarity purpose*)
type entry = (constr, types) kind_of_term
-(* the following types correspond to the different "things"
+(** the following types correspond to the different "things"
the kernel can learn about.*)
type nat_field =
| NatType
@@ -58,25 +56,26 @@ type int31_field =
| Int31Tail0
type field =
-(* | KEq
+
+(** | KEq
| KNat of nat_field
| KN of n_field *)
| KInt31 of string*int31_field
-(* This type represent an atomic action of the retroknowledge. It
- is stored in the compiled libraries *)
-(* As per now, there is only the possibility of registering things
+(** This type represent an atomic action of the retroknowledge. It
+ is stored in the compiled libraries
+ As per now, there is only the possibility of registering things
the possibility of unregistering or changing the flag is under study *)
type action =
| RKRegister of field*entry
-(* initial value for retroknowledge *)
+(** initial value for retroknowledge *)
val initial_retroknowledge : retroknowledge
-(* Given an identifier id (usually Const _)
+(** Given an identifier id (usually Const _)
and the continuation cont of the bytecode compilation
returns the compilation of id in cont if it has a specific treatment
or raises Not_found if id should be compiled as usual *)
@@ -103,28 +102,29 @@ val get_vm_constant_dynamic_info : retroknowledge -> entry ->
Cbytecodes.comp_env ->
Cbytecodes.block array ->
int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes
-(* Given a type identifier, this function is used before compiling a match
+
+(** Given a type identifier, this function is used before compiling a match
over this type. In the case of 31-bit integers for instance, it is used
to add the instruction sequence which would perform a dynamic decompilation
in case the argument of the match is not in coq representation *)
val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
-> Cbytecodes.bytecodes
-(* Given a type identifier, this function is used by pretyping/vnorm.ml to
+(** Given a type identifier, this function is used by pretyping/vnorm.ml to
recover the elements of that type from their compiled form if it's non
standard (it is used (and can be used) only when the compiled form
is not a block *)
val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
-(* the following functions are solely used in Pre_env and Environ to implement
+(** the following functions are solely used in Pre_env and Environ to implement
the functions register and unregister (and mem) of Environ *)
val add_field : retroknowledge -> field -> entry -> retroknowledge
val mem : retroknowledge -> field -> bool
val remove : retroknowledge -> field -> retroknowledge
val find : retroknowledge -> field -> entry
-(* the following function manipulate the reactive information of values
+(** the following function manipulate the reactive information of values
they are only used by the functions of Pre_env, and Environ to implement
the functions register and unregister of Environ *)
val add_vm_compiling_info : retroknowledge-> entry ->
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c378d8ccc..2aad2eb8c 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -1,22 +1,21 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Term
open Declarations
open Entries
open Mod_subst
-(*i*)
-(*s Safe environments. Since we are now able to type terms, we can
+(** {6 Sect } *)
+(** Safe environments. Since we are now able to type terms, we can
define an abstract type of safe environments, where objects are
typed before being added.
@@ -31,7 +30,7 @@ val env_of_safe_env : safe_environment -> Environ.env
val empty_environment : safe_environment
val is_empty : safe_environment -> bool
-(* Adding and removing local declarations (Local or Variables) *)
+(** Adding and removing local declarations (Local or Variables) *)
val push_named_assum :
identifier * types -> safe_environment ->
Univ.constraints * safe_environment
@@ -39,7 +38,7 @@ val push_named_def :
identifier * constr * types option -> safe_environment ->
Univ.constraints * safe_environment
-(* Adding global axioms or definitions *)
+(** Adding global axioms or definitions *)
type global_declaration =
| ConstantEntry of constant_entry
| GlobalRecipe of Cooking.recipe
@@ -48,30 +47,30 @@ val add_constant :
dir_path -> label -> global_declaration -> safe_environment ->
constant * safe_environment
-(* Adding an inductive type *)
+(** Adding an inductive type *)
val add_mind :
dir_path -> label -> mutual_inductive_entry -> safe_environment ->
mutual_inductive * safe_environment
-(* Adding a module *)
+(** Adding a module *)
val add_module :
label -> module_entry -> bool -> safe_environment
-> module_path * delta_resolver * safe_environment
-(* Adding a module type *)
+(** Adding a module type *)
val add_modtype :
label -> module_struct_entry -> bool -> safe_environment
-> module_path * safe_environment
-(* Adding universe constraints *)
+(** Adding universe constraints *)
val add_constraints :
Univ.constraints -> safe_environment -> safe_environment
-(* Settin the strongly constructive or classical logical engagement *)
+(** Settin the strongly constructive or classical logical engagement *)
val set_engagement : engagement -> safe_environment -> safe_environment
-(*s Interactive module functions *)
+(** {6 Interactive module functions } *)
val start_module :
label -> safe_environment -> module_path * safe_environment
@@ -96,9 +95,10 @@ val pack_module : safe_environment -> module_body
val current_modpath : safe_environment -> module_path
val delta_of_senv : safe_environment -> delta_resolver*delta_resolver
-(* Loading and saving compilation units *)
-(* exporting and importing modules *)
+(** Loading and saving compilation units *)
+
+(** exporting and importing modules *)
type compiled_library
val start_library : dir_path -> safe_environment
@@ -110,18 +110,18 @@ val export : safe_environment -> dir_path
val import : compiled_library -> Digest.t -> safe_environment
-> module_path * safe_environment
-(* Remove the body of opaque constants *)
+(** Remove the body of opaque constants *)
val lighten_library : compiled_library -> compiled_library
-(*s Typing judgments *)
+(** {6 Typing judgments } *)
type judgment
val j_val : judgment -> constr
val j_type : judgment -> constr
-(* Safe typing of a term returning a typing judgment and universe
+(** Safe typing of a term returning a typing judgment and universe
constraints to be added to the environment for the judgment to
hold. It is guaranteed that the constraints are satisfiable
*)
diff --git a/kernel/sign.mli b/kernel/sign.mli
index b3e7ace55..5cadb125f 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -1,19 +1,17 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Term
-(*i*)
-(*s Signatures of ordered named declarations *)
+(** {6 Signatures of ordered named declarations } *)
type named_context = named_declaration list
type section_context = named_context
@@ -24,39 +22,42 @@ val vars_of_named_context : named_context -> identifier list
val lookup_named : identifier -> named_context -> named_declaration
-(* number of declarations *)
+(** number of declarations *)
val named_context_length : named_context -> int
-(*s Recurrence on [named_context]: older declarations processed first *)
+(** {6 Recurrence on [named_context]: older declarations processed first } *)
val fold_named_context :
(named_declaration -> 'a -> 'a) -> named_context -> init:'a -> 'a
-(* newer declarations first *)
+
+(** newer declarations first *)
val fold_named_context_reverse :
('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
-(*s Section-related auxiliary functions *)
+(** {6 Section-related auxiliary functions } *)
val instance_from_named_context : named_context -> constr array
-(*s Signatures of ordered optionally named variables, intended to be
+(** {6 Sect } *)
+(** Signatures of ordered optionally named variables, intended to be
accessed by de Bruijn indices *)
val push_named_to_rel_context : named_context -> rel_context -> rel_context
-(*s Recurrence on [rel_context]: older declarations processed first *)
+(** {6 Recurrence on [rel_context]: older declarations processed first } *)
val fold_rel_context :
(rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
-(* newer declarations first *)
+
+(** newer declarations first *)
val fold_rel_context_reverse :
('a -> rel_declaration -> 'a) -> init:'a -> rel_context -> 'a
-(*s Map function of [rel_context] *)
+(** {6 Map function of [rel_context] } *)
val map_rel_context : (constr -> constr) -> rel_context -> rel_context
-(*s Map function of [named_context] *)
+(** {6 Map function of [named_context] } *)
val map_named_context : (constr -> constr) -> named_context -> named_context
-(*s Map function of [rel_context] *)
+(** {6 Map function of [rel_context] } *)
val iter_rel_context : (constr -> unit) -> rel_context -> unit
-(*s Map function of [named_context] *)
+(** {6 Map function of [named_context] } *)
val iter_named_context : (constr -> unit) -> named_context -> unit
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index c0b1ee5d3..d68d908a0 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -1,18 +1,16 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Univ
open Declarations
open Environ
-(*i*)
val check_subtypes : env -> module_type_body -> module_type_body -> constraints
diff --git a/kernel/term.mli b/kernel/term.mli
index ff71c3594..830e7e5ed 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -1,164 +1,172 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
-(*i*)
-(*s The sorts of CCI. *)
+(** {6 The sorts of CCI. } *)
type contents = Pos | Null
type sorts =
- | Prop of contents (* Prop and Set *)
- | Type of Univ.universe (* Type *)
+ | Prop of contents (** Prop and Set *)
+ | Type of Univ.universe (** Type *)
val set_sort : sorts
val prop_sort : sorts
val type1_sort : sorts
-(*s The sorts family of CCI. *)
+(** {6 The sorts family of CCI. } *)
type sorts_family = InProp | InSet | InType
val family_of_sort : sorts -> sorts_family
-(*s Useful types *)
+(** {6 Useful types } *)
-(*s Existential variables *)
+(** {6 Existential variables } *)
type existential_key = int
-(*s Existential variables *)
+(** {6 Existential variables } *)
type metavariable = int
-(*s Case annotation *)
-type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle
+(** {6 Case annotation } *)
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *)
type case_printing =
- { ind_nargs : int; (* length of the arity of the inductive type *)
+ { ind_nargs : int; (** length of the arity of the inductive type *)
style : case_style }
-(* the integer is the number of real args, needed for reduction *)
+
+(** the integer is the number of real args, needed for reduction *)
type case_info =
- { ci_ind : inductive;
- ci_npar : int;
- ci_cstr_ndecls : int array; (* number of pattern vars of each constructor *)
- ci_pp_info : case_printing (* not interpreted by the kernel *)
+ { ci_ind : inductive;
+ ci_npar : int;
+ ci_cstr_ndecls : int array; (** number of real args of each constructor *)
+ ci_pp_info : case_printing (** not interpreted by the kernel *)
}
-(*s*******************************************************************)
-(* The type of constructions *)
+(** {6 The type of constructions } *)
type constr
-(* [eq_constr a b] is true if [a] equals [b] modulo alpha, casts,
+(** [eq_constr a b] is true if [a] equals [b] modulo alpha, casts,
and application grouping *)
val eq_constr : constr -> constr -> bool
-(* [types] is the same as [constr] but is intended to be used for
+(** [types] is the same as [constr] but is intended to be used for
documentation to indicate that such or such function specifically works
- with {\em types} (i.e. terms of type a sort).
+ with {e types} (i.e. terms of type a sort).
(Rem:plurial form since [type] is a reserved ML keyword) *)
type types = constr
-(*s Functions for dealing with constr terms.
+(** {6 Sect } *)
+(** Functions for dealing with constr terms.
The following functions are intended to simplify and to uniform the
manipulation of terms. Some of these functions may be overlapped with
previous ones. *)
-(*s Term constructors. *)
+(** {6 Term constructors. } *)
-(* Constructs a DeBrujin index (DB indices begin at 1) *)
+(** Constructs a DeBrujin index (DB indices begin at 1) *)
val mkRel : int -> constr
-(* Constructs a Variable *)
+(** Constructs a Variable *)
val mkVar : identifier -> constr
-(* Constructs an patvar named "?n" *)
+(** Constructs an patvar named "?n" *)
val mkMeta : metavariable -> constr
-(* Constructs an existential variable *)
+(** Constructs an existential variable *)
type existential = existential_key * constr array
val mkEvar : existential -> constr
-(* Construct a sort *)
+(** Construct a sort *)
val mkSort : sorts -> types
val mkProp : types
val mkSet : types
val mkType : Univ.universe -> types
-(* This defines the strategy to use for verifiying a Cast *)
+(** This defines the strategy to use for verifiying a Cast *)
type cast_kind = VMcast | DEFAULTcast
-(* Constructs the term [t1::t2], i.e. the term $t_1$ casted with the
- type $t_2$ (that means t2 is declared as the type of t1). *)
+(** Constructs the term [t1::t2], i.e. the term {% $ %}t_1{% $ %} casted with the
+ type {% $ %}t_2{% $ %} (that means t2 is declared as the type of t1). *)
val mkCast : constr * cast_kind * constr -> constr
-(* Constructs the product [(x:t1)t2] *)
+(** Constructs the product [(x:t1)t2] *)
val mkProd : name * types * types -> types
val mkNamedProd : identifier -> types -> types -> types
-(* non-dependant product $t_1 \rightarrow t_2$, an alias for
- [(_:t1)t2]. Beware $t_2$ is NOT lifted.
+
+(** non-dependant product {% $ %}t_1 \rightarrow t_2{% $ %}, an alias for
+ [(_:t1)t2]. Beware {% $ %}t_2{% $ %} is NOT lifted.
Eg: A |- A->A is built by [(mkArrow (mkRel 0) (mkRel 1))] *)
val mkArrow : types -> types -> constr
-(* Constructs the abstraction $[x:t_1]t_2$ *)
+(** Constructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
val mkLambda : name * types * constr -> constr
val mkNamedLambda : identifier -> types -> constr -> constr
-(* Constructs the product [let x = t1 : t2 in t3] *)
+(** Constructs the product [let x = t1 : t2 in t3] *)
val mkLetIn : name * constr * types * constr -> constr
val mkNamedLetIn : identifier -> constr -> types -> constr -> constr
-(* [mkApp (f,[| t_1; ...; t_n |]] constructs the application
- $(f~t_1~\dots~t_n)$. *)
+(** [mkApp (f,[| t_1; ...; t_n |]] constructs the application
+ {% $ %}(f~t_1~\dots~t_n){% $ %}. *)
val mkApp : constr * constr array -> constr
-(* Constructs a constant *)
-(* The array of terms correspond to the variables introduced in the section *)
+(** Constructs a constant
+ The array of terms correspond to the variables introduced in the section *)
val mkConst : constant -> constr
-(* Inductive types *)
+(** Inductive types *)
-(* Constructs the ith (co)inductive type of the block named kn *)
-(* The array of terms correspond to the variables introduced in the section *)
+(** Constructs the ith (co)inductive type of the block named kn
+ The array of terms correspond to the variables introduced in the section *)
val mkInd : inductive -> constr
-(* Constructs the jth constructor of the ith (co)inductive type of the
+(** Constructs the jth constructor of the ith (co)inductive type of the
block named kn. The array of terms correspond to the variables
introduced in the section *)
val mkConstruct : constructor -> constr
-(* Constructs the term <p>Case c of c1 | c2 .. | cn end *)
+(** Construct the term <p>Case c of c1 | c2 .. | cn end
+
+ [mkCase ci p c ac] stand for match [c] return [p] with [ac] presented as
+ describe in [ci].
+
+ [p] stucture is lambda inductive_args, I inductive_args -> "return"
+
+ [ac]{^ ith} element is ith constructor case presented as
+ {e lambda construct_args (without params). case_term } *)
val mkCase : case_info * constr * constr * constr array -> constr
-(* If [recindxs = [|i1,...in|]]
+(** If [recindxs = [|i1,...in|]]
[funnames = [|f1,.....fn|]]
[typarray = [|t1,...tn|]]
[bodies = [|b1,.....bn|]]
- then [ mkFix ((recindxs,i), funnames, typarray, bodies) ]
- constructs the $i$th function of the block (counting from 0)
+ then [mkFix ((recindxs,i), funnames, typarray, bodies) ]
+ constructs the {% $ %}i{% $ %}th function of the block (counting from 0)
[Fixpoint f1 [ctx1] = b1
with f2 [ctx2] = b2
...
with fn [ctxn] = bn.]
- \noindent where the length of the $j$th context is $ij$.
+ \noindent where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
*)
type rec_declaration = name array * types array * constr array
type fixpoint = (int array * int) * rec_declaration
val mkFix : fixpoint -> constr
-(* If [funnames = [|f1,.....fn|]]
+(** If [funnames = [|f1,.....fn|]]
[typarray = [|t1,...tn|]]
[bodies = [b1,.....bn]] \par\noindent
then [mkCoFix (i, (funnames, typarray, bodies))]
@@ -173,9 +181,9 @@ type cofixpoint = int * rec_declaration
val mkCoFix : cofixpoint -> constr
-(*s Concrete type for making pattern-matching. *)
+(** {6 Concrete type for making pattern-matching. } *)
-(* [constr array] is an instance matching definitional [named_context] in
+(** [constr array] is an instance matching definitional [named_context] in
the same order (i.e. last argument first) *)
type 'constr pexistential = existential_key * 'constr array
type ('constr, 'types) prec_declaration =
@@ -203,14 +211,14 @@ type ('constr, 'types) kind_of_term =
| Fix of ('constr, 'types) pfixpoint
| CoFix of ('constr, 'types) pcofixpoint
-(* User view of [constr]. For [App], it is ensured there is at
+(** User view of [constr]. For [App], it is ensured there is at
least one argument and the function is not itself an applicative
term *)
val kind_of_term : constr -> (constr, types) kind_of_term
val kind_of_term2 : constr -> ((constr,types) kind_of_term,constr) kind_of_term
-(* Experimental *)
+(** Experimental *)
type ('constr, 'types) kind_of_type =
| SortType of sorts
| CastType of 'types * 'types
@@ -220,7 +228,7 @@ type ('constr, 'types) kind_of_type =
val kind_of_type : types -> (constr, types) kind_of_type
-(*s Simple term case analysis. *)
+(** {6 Simple term case analysis. } *)
val isRel : constr -> bool
val isVar : constr -> bool
@@ -247,75 +255,77 @@ val is_Type : constr -> bool
val iskind : constr -> bool
val is_small : sorts -> bool
-(*s Term destructors.
+(** {6 Sect } *)
+(** Term destructors.
Destructor operations are partial functions and
raise [invalid_arg "dest*"] if the term has not the expected form. *)
-(* Destructs a DeBrujin index *)
+(** Destructs a DeBrujin index *)
val destRel : constr -> int
-(* Destructs an existential variable *)
+(** Destructs an existential variable *)
val destMeta : constr -> metavariable
-(* Destructs a variable *)
+(** Destructs a variable *)
val destVar : constr -> identifier
-(* Destructs a sort. [is_Prop] recognizes the sort \textsf{Prop}, whether
- [isprop] recognizes both \textsf{Prop} and \textsf{Set}. *)
+(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
+ [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
val destSort : constr -> sorts
-(* Destructs a casted term *)
+(** Destructs a casted term *)
val destCast : constr -> constr * cast_kind * constr
-(* Destructs the product $(x:t_1)t_2$ *)
+(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *)
val destProd : types -> name * types * types
-(* Destructs the abstraction $[x:t_1]t_2$ *)
+(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *)
val destLambda : constr -> name * types * constr
-(* Destructs the let $[x:=b:t_1]t_2$ *)
+(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *)
val destLetIn : constr -> name * constr * types * constr
-(* Destructs an application *)
+(** Destructs an application *)
val destApp : constr -> constr * constr array
-(* Obsolete synonym of destApp *)
+(** Obsolete synonym of destApp *)
val destApplication : constr -> constr * constr array
-(* Decompose any term as an applicative term; the list of args can be empty *)
+(** Decompose any term as an applicative term; the list of args can be empty *)
val decompose_app : constr -> constr * constr list
-(* Destructs a constant *)
+(** Destructs a constant *)
val destConst : constr -> constant
-(* Destructs an existential variable *)
+(** Destructs an existential variable *)
val destEvar : constr -> existential
-(* Destructs a (co)inductive type *)
+(** Destructs a (co)inductive type *)
val destInd : constr -> inductive
-(* Destructs a constructor *)
+(** Destructs a constructor *)
val destConstruct : constr -> constructor
-(* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
+(** Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
val destCase : constr -> case_info * constr * constr * constr array
-(* Destructs the $i$th function of the block
- $\mathit{Fixpoint} ~ f_1 ~ [ctx_1] = b_1
- \mathit{with} ~ f_2 ~ [ctx_2] = b_2
+(** Destructs the {% $ %}i{% $ %}th function of the block
+ {% $ %}{% \mathit{%}Fixpoint{% }%} ~ f_1 ~ [ctx_1] = b_1
+ {% \mathit{%}with{% }%} ~ f_2 ~ [ctx_2] = b_2
\dots
- \mathit{with} ~ f_n ~ [ctx_n] = b_n$,
- where the lenght of the $j$th context is $ij$.
+ {% \mathit{%}with{% }%} ~ f_n ~ [ctx_n] = b_n{% $ %},
+ where the lenght of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}.
*)
val destFix : constr -> fixpoint
val destCoFix : constr -> cofixpoint
-(*s A {\em declaration} has the form (name,body,type). It is either an
- {\em assumption} if [body=None] or a {\em definition} if
- [body=Some actualbody]. It is referred by {\em name} if [na] is an
- identifier or by {\em relative index} if [na] is not an identifier
+(** {6 Sect } *)
+(** A {e declaration} has the form (name,body,type). It is either an
+ {e assumption} if [body=None] or a {e definition} if
+ [body=Some actualbody]. It is referred by {e name} if [na] is an
+ identifier or by {e relative index} if [na] is not an identifier
(in the latter case, [na] is of type [name] but just for printing
purpose *)
@@ -332,9 +342,9 @@ val fold_named_declaration :
val fold_rel_declaration :
(constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
-(*s Contexts of declarations referred to by de Bruijn indices *)
+(** {6 Contexts of declarations referred to by de Bruijn indices } *)
-(* In [rel_context], more recent declaration is on top *)
+(** In [rel_context], more recent declaration is on top *)
type rel_context = rel_declaration list
val empty_rel_context : rel_context
@@ -344,185 +354,186 @@ val lookup_rel : int -> rel_context -> rel_declaration
val rel_context_length : rel_context -> int
val rel_context_nhyps : rel_context -> int
-(* Constructs either [(x:t)c] or [[x=b:t]c] *)
+(** Constructs either [(x:t)c] or [[x=b:t]c] *)
val mkProd_or_LetIn : rel_declaration -> types -> types
val mkNamedProd_or_LetIn : named_declaration -> types -> types
val mkNamedProd_wo_LetIn : named_declaration -> types -> types
-(* Constructs either [[x:t]c] or [[x=b:t]c] *)
+(** Constructs either [[x:t]c] or [[x=b:t]c] *)
val mkLambda_or_LetIn : rel_declaration -> constr -> constr
val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
-(*s Other term constructors. *)
+(** {6 Other term constructors. } *)
val abs_implicit : constr -> constr
val lambda_implicit : constr -> constr
val lambda_implicit_lift : int -> constr -> constr
-(* [applist (f,args)] and co work as [mkApp] *)
+(** [applist (f,args)] and co work as [mkApp] *)
val applist : constr * constr list -> constr
val applistc : constr -> constr list -> constr
val appvect : constr * constr array -> constr
val appvectc : constr -> constr array -> constr
-(* [prodn n l b] = $(x_1:T_1)..(x_n:T_n)b$
- where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *)
+(** [prodn n l b] = {% $ %}(x_1:T_1)..(x_n:T_n)b{% $ %}
+ where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]{% $ %} *)
val prodn : int -> (name * constr) list -> constr -> constr
-(* [compose_prod l b] = $(x_1:T_1)..(x_n:T_n)b$
- where $l = [(x_n,T_n);\dots;(x_1,T_1)]$.
+(** [compose_prod l b] = {% $ %}(x_1:T_1)..(x_n:T_n)b{% $ %}
+ where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1)]{% $ %}.
Inverse of [decompose_prod]. *)
val compose_prod : (name * constr) list -> constr -> constr
-(* [lamn n l b] = $[x_1:T_1]..[x_n:T_n]b$
- where $l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]$ *)
+(** [lamn n l b] = {% $ %}[x_1:T_1]..[x_n:T_n]b{% $ %}
+ where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]{% $ %} *)
val lamn : int -> (name * constr) list -> constr -> constr
-(* [compose_lam l b] = $[x_1:T_1]..[x_n:T_n]b$
- where $l = [(x_n,T_n);\dots;(x_1,T_1)]$.
+(** [compose_lam l b] = {% $ %}[x_1:T_1]..[x_n:T_n]b{% $ %}
+ where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1)]{% $ %}.
Inverse of [it_destLam] *)
val compose_lam : (name * constr) list -> constr -> constr
-(* [to_lambda n l]
- = $[x_1:T_1]...[x_n:T_n]T$
- where $l = (x_1:T_1)...(x_n:T_n)T$ *)
+(** [to_lambda n l]
+ = {% $ %}[x_1:T_1]...[x_n:T_n]T{% $ %}
+ where {% $ %}l = (x_1:T_1)...(x_n:T_n)T{% $ %} *)
val to_lambda : int -> constr -> constr
-(* [to_prod n l]
- = $(x_1:T_1)...(x_n:T_n)T$
- where $l = [x_1:T_1]...[x_n:T_n]T$ *)
+(** [to_prod n l]
+ = {% $ %}(x_1:T_1)...(x_n:T_n)T{% $ %}
+ where {% $ %}l = [x_1:T_1]...[x_n:T_n]T{% $ %} *)
val to_prod : int -> constr -> constr
-(* pseudo-reduction rule *)
+(** pseudo-reduction rule *)
-(* [prod_appvect] $(x1:B1;...;xn:Bn)B a1...an \rightarrow B[a1...an]$ *)
+(** [prod_appvect] {% $ %}(x1:B1;...;xn:Bn)B a1...an \rightarrow B[a1...an]{% $ %} *)
val prod_appvect : constr -> constr array -> constr
val prod_applist : constr -> constr list -> constr
val it_mkLambda_or_LetIn : constr -> rel_context -> constr
val it_mkProd_or_LetIn : types -> rel_context -> types
-(*s Other term destructors. *)
+(** {6 Other term destructors. } *)
-(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ into the pair
- $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a product.
+(** Transforms a product term {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %} into the pair
+ {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a product.
It includes also local definitions *)
val decompose_prod : constr -> (name*constr) list * constr
-(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ into the pair
- $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a lambda. *)
+(** Transforms a lambda term {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair
+ {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *)
val decompose_lam : constr -> (name*constr) list * constr
-(* Given a positive integer n, transforms a product term
- $(x_1:T_1)..(x_n:T_n)T$
- into the pair $([(xn,Tn);...;(x1,T1)],T)$. *)
+(** Given a positive integer n, transforms a product term
+ {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %}
+ into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *)
val decompose_prod_n : int -> constr -> (name * constr) list * constr
-(* Given a positive integer $n$, transforms a lambda term
- $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *)
+(** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term
+ {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *)
val decompose_lam_n : int -> constr -> (name * constr) list * constr
-(* Extract the premisses and the conclusion of a term of the form
+(** Extract the premisses and the conclusion of a term of the form
"(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
val decompose_prod_assum : types -> rel_context * types
-(* Idem with lambda's *)
+(** Idem with lambda's *)
val decompose_lam_assum : constr -> rel_context * constr
-(* Idem but extract the first [n] premisses *)
+(** Idem but extract the first [n] premisses *)
val decompose_prod_n_assum : int -> types -> rel_context * types
val decompose_lam_n_assum : int -> constr -> rel_context * constr
-(* [nb_lam] $[x_1:T_1]...[x_n:T_n]c$ where $c$ is not an abstraction
- gives $n$ (casts are ignored) *)
+(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
+ gives {% $ %}n{% $ %} (casts are ignored) *)
val nb_lam : constr -> int
-(* Similar to [nb_lam], but gives the number of products instead *)
+(** Similar to [nb_lam], but gives the number of products instead *)
val nb_prod : constr -> int
-(* Returns the premisses/parameters of a type/term (let-in included) *)
+(** Returns the premisses/parameters of a type/term (let-in included) *)
val prod_assum : types -> rel_context
val lam_assum : constr -> rel_context
-(* Returns the first n-th premisses/parameters of a type/term (let included)*)
+(** Returns the first n-th premisses/parameters of a type/term (let included)*)
val prod_n_assum : int -> types -> rel_context
val lam_n_assum : int -> constr -> rel_context
-(* Remove the premisses/parameters of a type/term *)
+(** Remove the premisses/parameters of a type/term *)
val strip_prod : types -> types
val strip_lam : constr -> constr
-(* Remove the first n-th premisses/parameters of a type/term *)
+(** Remove the first n-th premisses/parameters of a type/term *)
val strip_prod_n : int -> types -> types
val strip_lam_n : int -> constr -> constr
-(* Remove the premisses/parameters of a type/term (including let-in) *)
+(** Remove the premisses/parameters of a type/term (including let-in) *)
val strip_prod_assum : types -> types
val strip_lam_assum : constr -> constr
-(* flattens application lists *)
+(** flattens application lists *)
val collapse_appl : constr -> constr
-(* Removes recursively the casts around a term i.e.
- [strip_outer_cast] (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
+(** Removes recursively the casts around a term i.e.
+ [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
val strip_outer_cast : constr -> constr
-(* Apply a function letting Casted types in place *)
+(** Apply a function letting Casted types in place *)
val under_casts : (constr -> constr) -> constr -> constr
-(* Apply a function under components of Cast if any *)
+(** Apply a function under components of Cast if any *)
val under_outer_cast : (constr -> constr) -> constr -> constr
-(*s An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
+(** {6 Sect } *)
+(** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort.
Such a term can canonically be seen as the pair of a context of types
and of a sort *)
type arity = rel_context * sorts
-(* Build an "arity" from its canonical form *)
+(** Build an "arity" from its canonical form *)
val mkArity : arity -> types
-(* Destructs an "arity" into its canonical form *)
+(** Destructs an "arity" into its canonical form *)
val destArity : types -> arity
-(* Tells if a term has the form of an arity *)
+(** Tells if a term has the form of an arity *)
val isArity : types -> bool
-(*s Occur checks *)
+(** {6 Occur checks } *)
-(* [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
+(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
val closedn : int -> constr -> bool
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
val closed0 : constr -> bool
-(* [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *)
+(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *)
val noccurn : int -> constr -> bool
-(* [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M]
+(** [noccur_between n m M] returns true iff [Rel p] does NOT occur in term [M]
for n <= p < n+m *)
val noccur_between : int -> int -> constr -> bool
-(* Checking function for terms containing existential- or
+(** Checking function for terms containing existential- or
meta-variables. The function [noccur_with_meta] does not consider
meta-variables applied to some terms (intented to be its local
context) (for existential variables, it is necessarily the case) *)
val noccur_with_meta : int -> int -> constr -> bool
-(*s Relocation and substitution *)
+(** {6 Relocation and substitution } *)
-(* [exliftn el c] lifts [c] with lifting [el] *)
+(** [exliftn el c] lifts [c] with lifting [el] *)
val exliftn : Esubst.lift -> constr -> constr
-(* [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
+(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
val liftn : int -> int -> constr -> constr
-(* [lift n c] lifts by [n] the positive indexes in [c] *)
+(** [lift n c] lifts by [n] the positive indexes in [c] *)
val lift : int -> constr -> constr
-(* [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
+(** [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
accordingly indexes in [a1],...,[an] *)
val substnl : constr list -> int -> constr -> constr
@@ -539,29 +550,30 @@ val substl_named_decl : constr list -> named_declaration -> named_declaration
val replace_vars : (identifier * constr) list -> constr -> constr
val subst_var : identifier -> constr -> constr
-(* [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
+(** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
if two names are identical, the one of least indice is kept *)
val subst_vars : identifier list -> constr -> constr
-(* [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
+
+(** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
if two names are identical, the one of least indice is kept *)
val substn_vars : int -> identifier list -> constr -> constr
-(*s Functionals working on the immediate subterm of a construction *)
+(** {6 Functionals working on the immediate subterm of a construction } *)
-(* [fold_constr f acc c] folds [f] on the immediate subterms of [c]
+(** [fold_constr f acc c] folds [f] on the immediate subterms of [c]
starting from [acc] and proceeding from left to right according to
the usual representation of the constructions; it is not recursive *)
val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a
-(* [map_constr f c] maps [f] on the immediate subterms of [c]; it is
+(** [map_constr f c] maps [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
val map_constr : (constr -> constr) -> constr -> constr
-(* [map_constr_with_binders g f n c] maps [f n] on the immediate
+(** [map_constr_with_binders g f n c] maps [f n] on the immediate
subterms of [c]; it carries an extra data [n] (typically a lift
index) which is processed by [g] (which typically add 1 to [n]) at
each binder traversal; it is not recursive and the order with which
@@ -570,13 +582,13 @@ val map_constr : (constr -> constr) -> constr -> constr
val map_constr_with_binders :
('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
-(* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
+(** [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
val iter_constr : (constr -> unit) -> constr -> unit
-(* [iter_constr_with_binders g f n c] iters [f n] on the immediate
+(** [iter_constr_with_binders g f n c] iters [f n] on the immediate
subterms of [c]; it carries an extra data [n] (typically a lift
index) which is processed by [g] (which typically add 1 to [n]) at
each binder traversal; it is not recursive and the order with which
@@ -585,7 +597,7 @@ val iter_constr : (constr -> unit) -> constr -> unit
val iter_constr_with_binders :
('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
-(* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
+(** [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
the immediate subterms of [c1] of [c2] if needed; Cast's, binders
name and Cases annotations are not taken into account *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 69b13e3b8..d1fc71eb5 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -1,14 +1,13 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Term
open Univ
@@ -17,7 +16,6 @@ open Inductive
open Environ
open Entries
open Typeops
-(*i*)
val translate_local_def : env -> constr * types option ->
constr * types * Univ.constraints
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 9c7b6561c..ed2ec1302 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -1,30 +1,28 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Term
open Environ
-(*i*)
-(* Type errors. \label{typeerrors} *)
+(** Type errors. {% \label{%}typeerrors{% }%} *)
(*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix
notation i*)
type guard_error =
- (* Fixpoints *)
+ (** Fixpoints *)
| NotEnoughAbstractionInFixBody
| RecursionNotOnInductiveType of constr
| RecursionOnIllegalTerm of int * constr * int list * int list
| NotEnoughArgumentsForFixCall of int
- (* CoFixpoints *)
+ (** CoFixpoints *)
| CodomainNotInductiveType of constr
| NestedRecursiveOccurrences
| UnguardedRecursiveCall of constr
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index b0f15e75d..a89aae4d2 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,23 +1,21 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(*i*)
open Names
open Univ
open Term
open Environ
open Entries
open Declarations
-(*i*)
-(*s Typing functions (not yet tagged as safe) *)
+(** {6 Typing functions (not yet tagged as safe) } *)
val infer : env -> constr -> unsafe_judgment * constraints
val infer_v : env -> constr array -> unsafe_judgment array * constraints
@@ -27,56 +25,56 @@ val infer_local_decls :
env -> (identifier * local_entry) list
-> env * rel_context * constraints
-(*s Basic operations of the typing machine. *)
+(** {6 Basic operations of the typing machine. } *)
-(* If [j] is the judgement $c:t$, then [assumption_of_judgement env j]
- returns the type $c$, checking that $t$ is a sort. *)
+(** If [j] is the judgement {% $ %}c:t{% $ %}, then [assumption_of_judgement env j]
+ returns the type {% $ %}c{% $ %}, checking that {% $ %}t{% $ %} is a sort. *)
val assumption_of_judgment : env -> unsafe_judgment -> types
val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment
-(*s Type of sorts. *)
+(** {6 Type of sorts. } *)
val judge_of_prop_contents : contents -> unsafe_judgment
val judge_of_type : universe -> unsafe_judgment
-(*s Type of a bound variable. *)
+(** {6 Type of a bound variable. } *)
val judge_of_relative : env -> int -> unsafe_judgment
-(*s Type of variables *)
+(** {6 Type of variables } *)
val judge_of_variable : env -> variable -> unsafe_judgment
-(*s type of a constant *)
+(** {6 type of a constant } *)
val judge_of_constant : env -> constant -> unsafe_judgment
val judge_of_constant_knowing_parameters :
env -> constant -> unsafe_judgment array -> unsafe_judgment
-(*s Type of application. *)
+(** {6 Type of application. } *)
val judge_of_apply :
env -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment * constraints
-(*s Type of an abstraction. *)
+(** {6 Type of an abstraction. } *)
val judge_of_abstraction :
env -> name -> unsafe_type_judgment -> unsafe_judgment
-> unsafe_judgment
-(*s Type of a product. *)
+(** {6 Type of a product. } *)
val judge_of_product :
env -> name -> unsafe_type_judgment -> unsafe_type_judgment
-> unsafe_judgment
-(* s Type of a let in. *)
+(** s Type of a let in. *)
val judge_of_letin :
env -> name -> unsafe_judgment -> unsafe_type_judgment -> unsafe_judgment
-> unsafe_judgment
-(*s Type of a cast. *)
+(** {6 Type of a cast. } *)
val judge_of_cast :
env -> unsafe_judgment -> cast_kind -> unsafe_type_judgment ->
unsafe_judgment * constraints
-(*s Inductive types. *)
+(** {6 Inductive types. } *)
val judge_of_inductive : env -> inductive -> unsafe_judgment
@@ -85,16 +83,16 @@ val judge_of_inductive_knowing_parameters :
val judge_of_constructor : env -> constructor -> unsafe_judgment
-(*s Type of Cases. *)
+(** {6 Type of Cases. } *)
val judge_of_case : env -> case_info
-> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
-> unsafe_judgment * constraints
-(* Typecheck general fixpoint (not checking guard conditions) *)
+(** Typecheck general fixpoint (not checking guard conditions) *)
val type_fixpoint : env -> name array -> types array
-> unsafe_judgment array -> constraints
-(* Kernel safe typing but applicable to partial proofs *)
+(** Kernel safe typing but applicable to partial proofs *)
val typing : env -> constr -> unsafe_judgment
val type_of_constant : env -> constant -> types
@@ -104,7 +102,7 @@ val type_of_constant_type : env -> constant_type -> types
val type_of_constant_knowing_parameters :
env -> constant_type -> constr array -> types
-(* Make a type polymorphic if an arity *)
+(** Make a type polymorphic if an arity *)
val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
constant_type
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 2bfcc2aa8..1d85386c5 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -1,23 +1,23 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
(*i $Id$ i*)
-(* Universes. *)
+(** Universes. *)
type universe
-(* The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... *)
-(* Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
+(** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ...
+ Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
-val type0m_univ : universe (* image of Prop in the universes hierarchy *)
-val type0_univ : universe (* image of Set in the universes hierarchy *)
-val type1_univ : universe (* the universe of the type of Prop/Set *)
+val type0m_univ : universe (** image of Prop in the universes hierarchy *)
+val type0_univ : universe (** image of Set in the universes hierarchy *)
+val type1_univ : universe (** the universe of the type of Prop/Set *)
val make_univ : Names.dir_path * int -> universe
@@ -25,13 +25,13 @@ val is_type0_univ : universe -> bool
val is_type0m_univ : universe -> bool
val is_univ_variable : universe -> bool
-(* The type of a universe *)
+(** The type of a universe *)
val super : universe -> universe
-(* The max of 2 universes *)
+(** The max of 2 universes *)
val sup : universe -> universe -> universe
-(*s Graphs of universes. *)
+(** {6 Graphs of universes. } *)
type universes
@@ -39,10 +39,10 @@ type check_function = universes -> universe -> universe -> bool
val check_geq : check_function
val check_eq : check_function
-(* The empty graph of universes *)
+(** The empty graph of universes *)
val initial_universes : universes
-(*s Constraints. *)
+(** {6 Constraints. } *)
module Constraint : Set.S
@@ -53,7 +53,8 @@ type constraint_function = universe -> universe -> constraints -> constraints
val enforce_geq : constraint_function
val enforce_eq : constraint_function
-(*s Merge of constraints in a universes graph.
+(** {6 Sect } *)
+(** Merge of constraints in a universes graph.
The function [merge_constraints] merges a set of constraints in a given
universes graph. It raises the exception [UniverseInconsistency] if the
constraints are not satisfiable. *)
@@ -64,7 +65,7 @@ exception UniverseInconsistency of order_request * universe * universe
val merge_constraints : constraints -> universes -> universes
-(*s Support for sort-polymorphic inductive types *)
+(** {6 Support for sort-polymorphic inductive types } *)
val fresh_local_univ : unit -> universe
@@ -78,13 +79,13 @@ val subst_large_constraints :
val no_upper_constraints : universe -> constraints -> bool
-(*s Pretty-printing of universes. *)
+(** {6 Pretty-printing of universes. } *)
val pr_uni : universe -> Pp.std_ppcmds
val pr_universes : universes -> Pp.std_ppcmds
val pr_constraints : constraints -> Pp.std_ppcmds
-(*s Dumping to a file *)
+(** {6 Dumping to a file } *)
val dump_universes : out_channel -> universes -> unit
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 551615aa5..6776821ed 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -1,20 +1,18 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(***********************************************************************
+ v * The Coq Proof Assistant / The Coq Development Team
+ <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud
+ \VV/ *************************************************************
+ // * This file is distributed under the terms of the
+ * GNU Lesser General Public License Version 2.1
+ ***********************************************************************)
-(*i*)
open Names
open Term
open Environ
open Reduction
-(*i*)
-(***********************************************************************)
-(*s conversion functions *)
+(**********************************************************************
+ s conversion functions *)
val use_vm : unit -> bool
val set_use_vm : bool -> unit
val vconv : conv_pb -> types conversion_function
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 5ecc8d99c..ff76e7cd5 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -8,10 +8,11 @@ val set_drawinstr : unit -> unit
val transp_values : unit -> bool
val set_transp_values : bool -> unit
-(* le code machine *)
+
+(** le code machine *)
type tcode
-(* Les valeurs ***********)
+(** Les valeurs ***********)
type vprod
type vfun
@@ -26,11 +27,11 @@ type atom =
| Aiddef of id_key * values
| Aind of inductive
-(* Les zippers *)
+(** Les zippers *)
type zipper =
| Zapp of arguments
- | Zfix of vfix*arguments (* Peut-etre vide *)
+ | Zfix of vfix*arguments (** Peut-etre vide *)
| Zswitch of vswitch
type stack = zipper list
@@ -64,42 +65,42 @@ external val_of_annot_switch : annot_switch -> values = "%identity"
(** Destructors *)
val whd_val : values -> whd
-(* Arguments *)
+(** Arguments *)
val nargs : arguments -> int
val arg : arguments -> int -> values
-(* Product *)
+(** Product *)
val dom : vprod -> values
val codom : vprod -> vfun
-(* Function *)
+(** Function *)
val body_of_vfun : int -> vfun -> values
val decompose_vfun2 : int -> vfun -> vfun -> int * values * values
-(* Fix *)
+(** Fix *)
val current_fix : vfix -> int
val check_fix : vfix -> vfix -> bool
val rec_args : vfix -> int array
val reduce_fix : int -> vfix -> vfun array * values array
- (* bodies , types *)
+ (** bodies , types *)
-(* CoFix *)
+(** CoFix *)
val current_cofix : vcofix -> int
val check_cofix : vcofix -> vcofix -> bool
val reduce_cofix : int -> vcofix -> values array * values array
- (* bodies , types *)
-(* Block *)
+ (** bodies , types
+ Block *)
val btag : vblock -> int
val bsize : vblock -> int
val bfield : vblock -> int -> values
-(* Switch *)
+(** Switch *)
val check_switch : vswitch -> vswitch -> bool
val case_info : vswitch -> case_info
val type_of_switch : vswitch -> values
val branch_of_switch : int -> vswitch -> (int * values) array
-(* Evaluation *)
+(** Evaluation *)
val whd_stack : values -> stack -> whd
val force_whd : values -> stack -> whd
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 11:21:19 +0000