aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
authorpboutill2010-04-29 09:56:37 +0000
committerpboutill2010-04-29 09:56:37 +0000
commitf73d7c4614d000f068550b5144d80b7eceed58e9 (patch)
tree4fa9a679a6e55269cc5c7cf24fce725acb2574b5 /pretyping
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 'pretyping')
-rw-r--r--pretyping/cases.mli18
-rw-r--r--pretyping/cbv.mli31
-rw-r--r--pretyping/classops.mli50
-rw-r--r--pretyping/coercion.mli32
-rw-r--r--pretyping/detyping.mli28
-rw-r--r--pretyping/evarconv.mli22
-rw-r--r--pretyping/evarutil.mli81
-rw-r--r--pretyping/evd.mli96
-rw-r--r--pretyping/indrec.mli30
-rw-r--r--pretyping/inductiveops.mli37
-rw-r--r--pretyping/matching.mli40
-rw-r--r--pretyping/namegen.mli46
-rw-r--r--pretyping/pattern.mli28
-rw-r--r--pretyping/pretype_errors.mli36
-rw-r--r--pretyping/pretyping.mli44
-rwxr-xr-xpretyping/recordops.mli46
-rw-r--r--pretyping/reductionops.mli62
-rw-r--r--pretyping/retyping.mli22
-rw-r--r--pretyping/tacred.mli49
-rw-r--r--pretyping/term_dnet.mli48
-rw-r--r--pretyping/termops.mli86
-rw-r--r--pretyping/typeclasses.mli34
-rw-r--r--pretyping/typeclasses_errors.mli20
-rw-r--r--pretyping/typing.mli30
-rw-r--r--pretyping/unification.mli28
-rw-r--r--pretyping/vnorm.mli18
26 files changed, 516 insertions, 546 deletions
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 6692403124..188959f6a6 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.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 Term
@@ -17,7 +16,6 @@ open Environ
open Inductiveops
open Rawterm
open Evarutil
-(*i*)
type pattern_matching_error =
| BadPattern of constructor * constr
@@ -47,7 +45,7 @@ val error_wrong_predicate_arity_loc : loc -> env -> constr -> constr -> constr -
val error_needs_inversion : env -> constr -> types -> 'a
val set_impossible_default_clause : constr * types -> unit
-(*s Compilation of pattern-matching. *)
+(** {6 Compilation of pattern-matching. } *)
type alias_constr =
| DepAlias
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index de66d22bce..75017d5b45 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -1,32 +1,30 @@
-(************************************************************************)
-(* 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
open Closure
open Esubst
-(*i*)
-(************************************************************************)
-(*s Call-by-value reduction *)
+(***********************************************************************
+ s Call-by-value reduction *)
-(* Entry point for cbv normalization of a constr *)
+(** Entry point for cbv normalization of a constr *)
type cbv_infos
val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos
val cbv_norm : cbv_infos -> constr -> constr
-(************************************************************************)
-(*i This is for cbv debug *)
+(***********************************************************************
+ i This is for cbv debug *)
type cbv_value =
| VAL of int * constr
| STACK of int * cbv_value * cbv_stack
@@ -46,7 +44,7 @@ val shift_value : int -> cbv_value -> cbv_value
val stack_app : cbv_value array -> cbv_stack -> cbv_stack
val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
-(* recursive functions... *)
+(** recursive functions... *)
val cbv_stack_term : cbv_infos ->
cbv_stack -> cbv_value subs -> constr -> cbv_value
val cbv_norm_term : cbv_infos -> cbv_value subs -> constr -> constr
@@ -54,4 +52,5 @@ val norm_head : cbv_infos ->
cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack
val apply_stack : cbv_infos -> constr -> cbv_stack -> constr
val cbv_norm_value : cbv_infos -> cbv_value -> constr
-(* End of cbv debug section i*)
+
+(** End of cbv debug section i*)
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 63d5b0a4e0..1830df3fbc 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.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 Decl_kinds
open Term
@@ -16,9 +15,8 @@ open Evd
open Environ
open Nametab
open Mod_subst
-(*i*)
-(*s This is the type of class kinds *)
+(** {6 This is the type of class kinds } *)
type cl_typ =
| CL_SORT
| CL_FUN
@@ -28,53 +26,53 @@ type cl_typ =
val subst_cl_typ : substitution -> cl_typ -> cl_typ
-(* This is the type of infos for declared classes *)
+(** This is the type of infos for declared classes *)
type cl_info_typ = {
cl_param : int }
-(* This is the type of coercion kinds *)
+(** This is the type of coercion kinds *)
type coe_typ = Libnames.global_reference
-(* This is the type of infos for declared coercions *)
+(** This is the type of infos for declared coercions *)
type coe_info_typ
-(* [cl_index] is the type of class keys *)
+(** [cl_index] is the type of class keys *)
type cl_index
-(* [coe_index] is the type of coercion keys *)
+(** [coe_index] is the type of coercion keys *)
type coe_index
-(* This is the type of paths from a class to another *)
+(** This is the type of paths from a class to another *)
type inheritance_path = coe_index list
-(*s Access to classes infos *)
+(** {6 Access to classes infos } *)
val class_info : cl_typ -> (cl_index * cl_info_typ)
val class_exists : cl_typ -> bool
val class_info_from_index : cl_index -> cl_typ * cl_info_typ
-(* [find_class_type env sigma c] returns the head reference of [c] and its
+(** [find_class_type env sigma c] returns the head reference of [c] and its
arguments *)
val find_class_type : env -> evar_map -> types -> cl_typ * constr list
-(* raises [Not_found] if not convertible to a class *)
+(** raises [Not_found] if not convertible to a class *)
val class_of : env -> evar_map -> types -> types * cl_index
-(* raises [Not_found] if not mapped to a class *)
+(** raises [Not_found] if not mapped to a class *)
val inductive_class_of : inductive -> cl_index
val class_args_of : env -> evar_map -> types -> constr list
-(*s [declare_coercion] adds a coercion in the graph of coercion paths *)
+(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
val declare_coercion :
coe_typ -> locality -> isid:bool ->
src:cl_typ -> target:cl_typ -> params:int -> unit
-(*s Access to coercions infos *)
+(** {6 Access to coercions infos } *)
val coercion_exists : coe_typ -> bool
val coercion_value : coe_index -> (unsafe_judgment * bool)
-(*s Lookup functions for coercion paths *)
+(** {6 Lookup functions for coercion paths } *)
val lookup_path_between_class : cl_index * cl_index -> inheritance_path
val lookup_path_between : env -> evar_map -> types * types ->
@@ -90,9 +88,9 @@ val lookup_pattern_path_between :
open Pp
val install_path_printer :
((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit
-(*i*)
+(**/**)
-(*s This is for printing purpose *)
+(** {6 This is for printing purpose } *)
val string_of_class : cl_typ -> string
val pr_class : cl_typ -> std_ppcmds
val pr_cl_index : cl_index -> std_ppcmds
@@ -101,6 +99,6 @@ val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
val classes : unit -> cl_typ list
val coercions : unit -> coe_index list
-(* [hide_coercion] returns the number of params to skip if the coercion must
+(** [hide_coercion] returns the number of params to skip if the coercion must
be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
val hide_coercion : coe_typ -> int option
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 565cf0c409..3ac83fc19d 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.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 Evd
open Names
@@ -17,34 +16,33 @@ open Sign
open Environ
open Evarutil
open Rawterm
-(*i*)
module type S = sig
- (*s Coercions. *)
+ (** {6 Coercions. } *)
- (* [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
+ (** [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
type a product; it returns [j] if no coercion is applicable *)
val inh_app_fun :
env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
- (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
+ (** [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
type a sort; it fails if no coercion is applicable *)
val inh_coerce_to_sort : loc ->
env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment
- (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+ (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
inserts a coercion into [j], if needed, in such a way it gets as
type its base type (the notion depends on the coercion system) *)
val inh_coerce_to_base : loc ->
env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
- (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+ (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
val inh_coerce_to_prod : loc ->
env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type
- (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
+ (** [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type
[t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
[j.uj_type] are convertible; it fails if no coercion is applicable *)
val inh_conv_coerce_to : loc ->
@@ -53,13 +51,13 @@ module type S = sig
val inh_conv_coerce_rigid_to : loc ->
env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment
- (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
+ (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
is coercible to an object of type [t'] adding evar constraints if needed;
it fails if no coercion exists *)
val inh_conv_coerces_to : loc ->
env -> evar_map -> types -> type_constraint_type -> evar_map
- (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
+ (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
pattern [pat] typed in [ind1] into a pattern typed in [ind2];
raises [Not_found] if no coercion found *)
val inh_pattern_coerce_to :
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index d7fb01aece..7b14c4fd2f 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.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 Term
@@ -17,16 +16,15 @@ open Environ
open Rawterm
open Termops
open Mod_subst
-(*i*)
val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
val subst_rawconstr : substitution -> rawconstr -> rawconstr
-(* [detype isgoal avoid ctx c] turns a closed [c], into a rawconstr *)
-(* de Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
-(* [isgoal] tells if naming must avoid global-level synonyms as intro does *)
-(* [ctx] gives the names of the free variables *)
+(** [detype isgoal avoid ctx c] turns a closed [c], into a rawconstr
+ de Bruijn indexes are turned to bound names, avoiding names in [avoid]
+ [isgoal] tells if naming must avoid global-level synonyms as intro does
+ [ctx] gives the names of the free variables *)
val detype : bool -> identifier list -> names_context -> constr -> rawconstr
@@ -43,7 +41,7 @@ val detype_sort : sorts -> rawsort
val detype_rel_context : constr option -> identifier list -> names_context ->
rel_context -> rawdecl list
-(* look for the index of a named var or a nondep var as it is renamed *)
+(** look for the index of a named var or a nondep var as it is renamed *)
val lookup_name_as_displayed : env -> constr -> identifier -> int option
val lookup_index_as_renamed : env -> constr -> int -> int option
@@ -51,7 +49,7 @@ val set_detype_anonymous : (loc -> int -> rawconstr) -> unit
val force_wildcard : unit -> bool
val synthetize_type : unit -> bool
-(* Utilities to transform kernel cases to simple pattern-matching problem *)
+(** Utilities to transform kernel cases to simple pattern-matching problem *)
val it_destRLambda_or_LetIn_names : int -> rawconstr -> name list * rawconstr
val simple_cases_matrix_of_branches :
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 28b960bb9f..2e52fb12b9 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.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 Term
open Sign
open Environ
open Reductionops
open Evd
-(*i*)
-(* returns exception Reduction.NotConvertible if not unifiable *)
+(** returns exception Reduction.NotConvertible if not unifiable *)
val the_conv_x : env -> constr -> constr -> evar_map -> evar_map
val the_conv_x_leq : env -> constr -> constr -> evar_map -> evar_map
-(* The same function resolving evars by side-effect and
+(** The same function resolving evars by side-effect and
catching the exception *)
val e_conv : env -> evar_map ref -> constr -> constr -> bool
val e_cumul : env -> evar_map ref -> constr -> constr -> bool
@@ -32,7 +30,7 @@ val evar_eqappr_x :
env -> evar_map ->
conv_pb -> constr * constr list -> constr * constr list ->
evar_map * bool
-(*i*)
+(**/**)
val consider_remaining_unif_problems : env -> evar_map -> evar_map
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 39f8dd05ac..3f66dc97e1 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.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 Rawterm
@@ -17,29 +16,29 @@ open Sign
open Evd
open Environ
open Reductionops
-(*i*)
-(*s This modules provides useful functions for unification modulo evars *)
+(** {6 This modules provides useful functions for unification modulo evars } *)
-(***********************************************************)
-(* Metas *)
+(**********************************************************
+ Metas *)
-(* [new_meta] is a generator of unique meta variables *)
+(** [new_meta] is a generator of unique meta variables *)
val new_meta : unit -> metavariable
val mk_new_meta : unit -> constr
-(* [new_untyped_evar] is a generator of unique evar keys *)
+(** [new_untyped_evar] is a generator of unique evar keys *)
val new_untyped_evar : unit -> existential_key
-(***********************************************************)
-(* Creating a fresh evar given their type and context *)
+(**********************************************************
+ Creating a fresh evar given their type and context *)
val new_evar :
evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_map * constr
-(* the same with side-effects *)
+
+(** the same with side-effects *)
val e_new_evar :
evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr
-(* Create a fresh evar in a context different from its definition context:
+(** Create a fresh evar in a context different from its definition context:
[new_evar_instance sign evd ty inst] creates a new evar of context
[sign] and type [ty], [inst] is a mapping of the evar context to
the context where the evar should occur. This means that the terms
@@ -50,30 +49,30 @@ val new_evar_instance :
val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
-(***********************************************************)
-(* Instantiate evars *)
+(**********************************************************
+ Instantiate evars *)
-(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
+(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
possibly solving related unification problems, possibly leaving open
some problems that cannot be solved in a unique way (except if choose is
true); fails if the instance is not valid for the given [ev] *)
val evar_define : ?choose:bool -> env -> existential -> constr -> evar_map -> evar_map
-(***********************************************************)
-(* Evars/Metas switching... *)
+(**********************************************************
+ Evars/Metas switching... *)
-(* [evars_to_metas] generates new metavariables for each non dependent
+(** [evars_to_metas] generates new metavariables for each non dependent
existential and performs the replacement in the given constr; it also
returns the evar_map extended with dependent evars *)
val evars_to_metas : evar_map -> open_constr -> (evar_map * constr)
val non_instantiated : evar_map -> (evar * evar_info) list
-(***********************************************************)
-(* Unification utils *)
+(**********************************************************
+ Unification utils *)
exception NoHeadEvar
-val head_evar : constr -> existential_key (* may raise NoHeadEvar *)
+val head_evar : constr -> existential_key (** may raise NoHeadEvar *)
val is_ground_term : evar_map -> constr -> bool
val is_ground_env : evar_map -> env -> bool
@@ -86,7 +85,7 @@ val solve_simple_eqn :
-> ?choose:bool -> env -> evar_map -> bool option * existential * constr ->
evar_map * bool
-(* [check_evars env initial_sigma extended_sigma c] fails if some
+(** [check_evars env initial_sigma extended_sigma c] fails if some
new unresolved evar remains in [c] *)
val check_evars : env -> evar_map -> evar_map -> constr -> unit
@@ -105,8 +104,8 @@ val evars_of_term : constr -> Intset.t
val evars_of_named_context : named_context -> Intset.t
val evars_of_evar_info : evar_info -> Intset.t
-(***********************************************************)
-(* Value/Type constraints *)
+(**********************************************************
+ Value/Type constraints *)
val judge_of_new_Type : unit -> unsafe_judgment
@@ -136,8 +135,8 @@ val lift_tycon : int -> type_constraint -> type_constraint
(***********************************************************)
-(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *)
-(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
+(** [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated;
+ *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *)
val nf_evar : evar_map -> constr -> constr
val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment
@@ -155,7 +154,7 @@ val nf_named_context_evar : evar_map -> named_context -> named_context
val nf_rel_context_evar : evar_map -> rel_context -> rel_context
val nf_env_evar : evar_map -> env -> env
-(* Same for evar defs *)
+(** Same for evar defs *)
val nf_isevar : evar_map -> constr -> constr
val j_nf_isevar : evar_map -> unsafe_judgment -> unsafe_judgment
val jl_nf_isevar :
@@ -167,25 +166,25 @@ val tj_nf_isevar :
val nf_evar_map : evar_map -> evar_map
-(* Replacing all evars *)
+(** Replacing all evars *)
exception Uninstantiated_evar of existential_key
val whd_ise : evar_map -> constr -> constr
val whd_castappevar : evar_map -> constr -> constr
-(* Replace the vars and rels that are aliases to other vars and rels by *)
-(* their representative that is most ancient in the context *)
+(** Replace the vars and rels that are aliases to other vars and rels by
+ their representative that is most ancient in the context *)
val expand_vars_in_term : env -> constr -> constr
-(*********************************************************************)
-(* debug pretty-printer: *)
+(********************************************************************
+ debug pretty-printer: *)
val pr_tycon_type : env -> type_constraint_type -> Pp.std_ppcmds
val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
-(*********************************************************************)
-(* Removing hyps in evars'context; *)
-(* raise OccurHypInSimpleClause if the removal breaks dependencies *)
+(********************************************************************
+ Removing hyps in evars'context;
+ raise OccurHypInSimpleClause if the removal breaks dependencies *)
type clear_dependency_error =
| OccurHypInSimpleClause of identifier option
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f895ead42c..2601d44f7e 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -1,15 +1,14 @@
-(************************************************************************)
-(* 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 Term
@@ -18,10 +17,9 @@ open Environ
open Libnames
open Mod_subst
open Termops
-(*i*)
-(*********************************************************************)
-(* Meta map *)
+(********************************************************************
+ Meta map *)
module Metamap : Map.S with type key = metavariable
@@ -37,7 +35,7 @@ val metavars_of : constr -> Metaset.t
val mk_freelisted : constr -> constr freelisted
val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
-(* Status of an instance found by unification wrt to the meta it solves:
+(** Status of an instance found by unification wrt to the meta it solves:
- a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
- a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
- a term that can be eta-expanded n times while still being a solution
@@ -47,7 +45,7 @@ val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
type instance_constraint =
IsSuperType | IsSubType | ConvUpToEta of int | UserGiven
-(* Status of the unification of the type of an instance against the type of
+(** Status of the unification of the type of an instance against the type of
the meta it instantiates:
- CoerceToType means that the unification of types has not been done
and that a coercion can still be inserted: the meta should not be
@@ -63,11 +61,11 @@ type instance_constraint =
type instance_typing_status =
CoerceToType | TypeNotProcessed | TypeProcessed
-(* Status of an instance together with the status of its type unification *)
+(** Status of an instance together with the status of its type unification *)
type instance_status = instance_constraint * instance_typing_status
-(* Clausal environments *)
+(** Clausal environments *)
type clbinding =
| Cltyp of name * constr freelisted
@@ -76,17 +74,17 @@ type clbinding =
val map_clb : (constr -> constr) -> clbinding -> clbinding
-(*********************************************************************)
-(*** Kinds of existential variables ***)
+(********************************************************************
+ ** Kinds of existential variables ***)
-(* Should the obligation be defined (opaque or transparent (default)) or
+(** Should the obligation be defined (opaque or transparent (default)) or
defined transparent and expanded in the term? *)
type obligation_definition_status = Define of bool | Expand
-(* Evars *)
+(** Evars *)
type hole_kind =
- | ImplicitArg of global_reference * (int * identifier option) * bool (* Force inference *)
+ | ImplicitArg of global_reference * (int * identifier option) * bool (** Force inference *)
| BinderType of name
| QuestionMark of obligation_definition_status
| CasesType
@@ -96,10 +94,10 @@ type hole_kind =
| ImpossibleCase
| MatchingVar of bool * identifier
-(*********************************************************************)
-(*** Existential variables and unification states ***)
+(********************************************************************
+ ** Existential variables and unification states ***)
-(* A unification state (of type [evar_map]) is primarily a finite mapping
+(** A unification state (of type [evar_map]) is primarily a finite mapping
from existential variables to records containing the type of the evar
([evar_concl]), the context under which it was introduced ([evar_hyps])
and its definition ([evar_body]). [evar_extra] is used to add any other
@@ -107,7 +105,7 @@ type hole_kind =
It also contains conversion constraints, debugging information and
information about meta variables. *)
-(* Information about existential variables. *)
+(** Information about existential variables. *)
type evar = existential_key
val string_of_existential : evar -> string
@@ -140,9 +138,9 @@ val evar_env : evar_info -> env
(*** Unification state ***)
type evar_map
-(* Unification state and existential variables *)
+(** Unification state and existential variables *)
-(* Assuming that the second map extends the first one, this says if
+(** Assuming that the second map extends the first one, this says if
some existing evar has been refined *)
val progress_evar_map : evar_map -> evar_map -> bool
@@ -166,7 +164,8 @@ val is_evar : evar_map -> evar -> bool
val is_defined : evar_map -> evar -> bool
-(*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
+(** {6 Sect } *)
+(** [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has
no body and [Not_found] if it does not exist in [sigma] *)
exception NotInstantiatedEvar
@@ -174,14 +173,14 @@ val existential_value : evar_map -> existential -> constr
val existential_type : evar_map -> existential -> types
val existential_opt_value : evar_map -> existential -> constr option
-(* Assume empty universe constraints in [evar_map] and [conv_pbs] *)
+(** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
val subst_evar_defs_light : substitution -> evar_map -> evar_map
-(* spiwack: this function seems to somewhat break the abstraction. *)
+(** spiwack: this function seems to somewhat break the abstraction. *)
val evars_reset_evd : evar_map -> evar_map -> evar_map
-(* spiwack: [is_undefined_evar] should be considered a candidate
+(** spiwack: [is_undefined_evar] should be considered a candidate
for moving to evarutils *)
val is_undefined_evar : evar_map -> constr -> bool
val undefined_evars : evar_map -> evar_map
@@ -199,11 +198,11 @@ val evar_declare :
?filter:bool list -> evar_map -> evar_map
val evar_source : existential_key -> evar_map -> loc * hole_kind
-(* spiwack: this function seems to somewhat break the abstraction. *)
-(* [evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
+(** spiwack: this function seems to somewhat break the abstraction.
+ [evar_merge evd ev1] extends the evars of [evd] with [evd1] *)
val evar_merge : evar_map -> evar_map -> evar_map
-(* Unification constraints *)
+(** Unification constraints *)
type conv_pb = Reduction.conv_pb
type evar_constraint = conv_pb * env * constr * constr
val add_conv_pb : evar_constraint -> evar_map -> evar_map
@@ -215,11 +214,12 @@ val extract_changed_conv_pbs : evar_map ->
val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list
-(* Metas *)
+(** Metas *)
val find_meta : evar_map -> metavariable -> clbinding
val meta_list : evar_map -> (metavariable * clbinding) list
val meta_defined : evar_map -> metavariable -> bool
-(* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
+
+(** [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if
meta has no value *)
val meta_value : evar_map -> metavariable -> constr
val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_status
@@ -233,7 +233,7 @@ val meta_declare :
val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map
val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map
-(* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
+(** [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *)
val meta_merge : evar_map -> evar_map -> evar_map
val undefined_metas : evar_map -> metavariable list
@@ -245,8 +245,8 @@ type metabinding = metavariable * constr * instance_status
val retract_coercible_metas : evar_map -> metabinding list * evar_map
val subst_defined_metas : metabinding list -> constr -> constr option
-(**********************************************************)
-(* Sort variables *)
+(*********************************************************
+ Sort variables *)
val new_sort_variable : evar_map -> sorts * evar_map
val is_sort_variable : evar_map -> sorts -> bool
@@ -254,12 +254,12 @@ val whd_sort_variable : evar_map -> constr -> constr
val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map
val define_sort_variable : evar_map -> sorts -> sorts -> evar_map
-(*********************************************************************)
-(* constr with holes *)
+(********************************************************************
+ constr with holes *)
type open_constr = evar_map * constr
-(*********************************************************************)
-(* The type constructor ['a sigma] adds an evar map to an object of
+(********************************************************************
+ The type constructor ['a sigma] adds an evar map to an object of
type ['a] *)
type 'a sigma = {
it : 'a ;
@@ -268,13 +268,13 @@ type 'a sigma = {
val sig_it : 'a sigma -> 'a
val sig_sig : 'a sigma -> evar_map
-(**********************************************************)
-(* Failure explanation *)
+(*********************************************************
+ Failure explanation *)
type unsolvability_explanation = SeveralInstancesFound of int
-(*********************************************************************)
-(* debug pretty-printer: *)
+(********************************************************************
+ debug pretty-printer: *)
val pr_evar_info : evar_info -> Pp.std_ppcmds
val pr_evar_map : evar_map -> Pp.std_ppcmds
@@ -282,8 +282,8 @@ val pr_sort_constraints : evar_map -> Pp.std_ppcmds
val pr_metaset : Metaset.t -> Pp.std_ppcmds
-(*** /!\Deprecated /!\ ***)
-(* create an [evar_map] with empty meta map: *)
+(*** /!\Deprecated /!\ **
+ create an [evar_map] with empty meta map: *)
val create_evar_defs : evar_map -> evar_map
val create_goal_evar_defs : evar_map -> evar_map
val is_defined_evar : evar_map -> existential -> bool
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 91d559e17e..304b986a16 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.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 Term
open Declarations
open Inductiveops
open Environ
open Evd
-(*i*)
-(* Errors related to recursors building *)
+(** Errors related to recursors building *)
type recursion_scheme_error =
| NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
@@ -29,35 +27,35 @@ exception RecursionSchemeError of recursion_scheme_error
type dep_flag = bool
-(* Build a case analysis elimination scheme in some sort family *)
+(** Build a case analysis elimination scheme in some sort family *)
val build_case_analysis_scheme : env -> evar_map -> inductive ->
dep_flag -> sorts_family -> constr
-(* Build a dependent case elimination predicate unless type is in Prop *)
+(** Build a dependent case elimination predicate unless type is in Prop *)
val build_case_analysis_scheme_default : env -> evar_map -> inductive ->
sorts_family -> constr
-(* Builds a recursive induction scheme (Peano-induction style) in the same
+(** Builds a recursive induction scheme (Peano-induction style) in the same
sort family as the inductive family; it is dependent if not in Prop *)
val build_induction_scheme : env -> evar_map -> inductive ->
dep_flag -> sorts_family -> constr
-(* Builds mutual (recursive) induction schemes *)
+(** Builds mutual (recursive) induction schemes *)
val build_mutual_induction_scheme :
env -> evar_map -> (inductive * dep_flag * sorts_family) list -> constr list
(** Scheme combinators *)
-(* [modify_sort_scheme s n c] modifies the quantification sort of
+(** [modify_sort_scheme s n c] modifies the quantification sort of
scheme c whose predicate is abstracted at position [n] of [c] *)
val modify_sort_scheme : sorts -> int -> constr -> constr
-(* [weaken_sort_scheme s n c t] derives by subtyping from [c:t]
+(** [weaken_sort_scheme s n c t] derives by subtyping from [c:t]
whose conclusion is quantified on [Type] at position [n] of [t] a
scheme quantified on sort [s] *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index a9a51d9ac5..6255a83d40 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.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*)
@@ -15,19 +15,19 @@ open Environ
open Evd
open Sign
-(* The following three functions are similar to the ones defined in
+(** The following three functions are similar to the ones defined in
Inductive, but they expect an env *)
val type_of_inductive : env -> inductive -> types
-(* Return type as quoted by the user *)
+(** Return type as quoted by the user *)
val type_of_constructor : env -> constructor -> types
val type_of_constructors : env -> inductive -> types array
-(* Return constructor types in normal form *)
+(** Return constructor types in normal form *)
val arities_of_constructors : env -> inductive -> types array
-(* An inductive type with its parameters *)
+(** An inductive type with its parameters *)
type inductive_family
val make_ind_family : inductive * constr list -> inductive_family
val dest_ind_family : inductive_family -> inductive * constr list
@@ -37,7 +37,7 @@ val lift_inductive_family : int -> inductive_family -> inductive_family
val substnl_ind_family :
constr list -> int -> inductive_family -> inductive_family
-(* An inductive type with its parameters and real arguments *)
+(** An inductive type with its parameters and real arguments *)
type inductive_type = IndType of inductive_family * constr list
val make_ind_type : inductive_family * constr list -> inductive_type
val dest_ind_type : inductive_type -> inductive_family * constr list
@@ -53,14 +53,15 @@ val mis_is_recursive :
val mis_nf_constructor_type :
inductive * mutual_inductive_body * one_inductive_body -> int -> constr
-(* Extract information from an inductive name *)
+(** Extract information from an inductive name *)
+(** Arity of constructors excluding parameters and local defs *)
val mis_constr_nargs : inductive -> int array
val mis_constr_nargs_env : env -> inductive -> int array
val nconstructors : inductive -> int
-(* Return the lengths of parameters signature and real arguments signature *)
+(** Return the lengths of parameters signature and real arguments signature *)
val inductive_nargs : env -> inductive -> int * int
val mis_constructor_nargs_env : env -> constructor -> int
@@ -71,7 +72,7 @@ val get_full_arity_sign : env -> inductive -> rel_context
val allowed_sorts : env -> inductive -> sorts_family list
-(* Extract information from an inductive family *)
+(** Extract information from an inductive family *)
type constructor_summary = {
cs_cstr : constructor;
@@ -92,7 +93,7 @@ val make_arity_signature : env -> bool -> inductive_family -> rel_context
val make_arity : env -> bool -> inductive_family -> sorts -> types
val build_branch_type : env -> bool -> constr -> constructor_summary -> types
-(* Raise [Not_found] if not given an valid inductive type *)
+(** Raise [Not_found] if not given an valid inductive type *)
val extract_mrectype : constr -> inductive * constr list
val find_mrectype : env -> evar_map -> constr -> inductive * constr list
val find_rectype : env -> evar_map -> constr -> inductive_type
@@ -101,13 +102,15 @@ val find_coinductive : env -> evar_map -> constr -> inductive * constr list
(********************)
-(* Builds the case predicate arity (dependent or not) *)
+(** Builds the case predicate arity (dependent or not) *)
val arity_of_case_predicate :
env -> inductive_family -> bool -> sorts -> types
val type_case_branches_with_names :
env -> inductive * constr list -> constr -> constr ->
types array * types
+
+(** Annotation for cases *)
val make_case_info : env -> inductive -> case_style -> case_info
(*i Compatibility
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 98d16b1128..263ded3814 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -1,22 +1,20 @@
-(************************************************************************)
-(* 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
open Pattern
open Termops
-(*i*)
-(*s This modules implements pattern-matching on terms *)
+(** {6 This modules implements pattern-matching on terms } *)
exception PatternMatchingFailure
@@ -24,56 +22,56 @@ val special_meta : metavariable
type bound_ident_map = (identifier * identifier) list
-(* [matches pat c] matches [c] against [pat] and returns the resulting
+(** [matches pat c] matches [c] against [pat] and returns the resulting
assignment of metavariables; it raises [PatternMatchingFailure] if
not matchable; bindings are given in increasing order based on the
numbers given in the pattern *)
val matches : constr_pattern -> constr -> patvar_map
-(* [extended_matches pat c] also returns the names of bound variables
+(** [extended_matches pat c] also returns the names of bound variables
in [c] that matches the bound variables in [pat]; if several bound
variables or metavariables have the same name, the metavariable,
or else the rightmost bound variable, takes precedence *)
val extended_matches :
constr_pattern -> constr -> bound_ident_map * patvar_map
-(* [is_matching pat c] just tells if [c] matches against [pat] *)
+(** [is_matching pat c] just tells if [c] matches against [pat] *)
val is_matching : constr_pattern -> constr -> bool
-(* [matches_conv env sigma] matches up to conversion in environment
+(** [matches_conv env sigma] matches up to conversion in environment
[(env,sigma)] when constants in pattern are concerned; it raises
[PatternMatchingFailure] if not matchable; bindings are given in
increasing order based on the numbers given in the pattern *)
val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
-(* The type of subterm matching results: a substitution + a context
+(** The type of subterm matching results: a substitution + a context
(whose hole is denoted with [special_meta]) + a continuation that
either returns the next matching subterm or raise PatternMatchingFailure *)
type subterm_matching_result =
(bound_ident_map * patvar_map) * constr * (unit -> subterm_matching_result)
-(* [match_subterm n pat c] returns the substitution and the context
+(** [match_subterm n pat c] returns the substitution and the context
corresponding to the first **closed** subterm of [c] matching [pat], and
a continuation that looks for the next matching subterm.
It raises PatternMatchingFailure if no subterm matches the pattern *)
val match_subterm : constr_pattern -> constr -> subterm_matching_result
-(* [match_appsubterm pat c] returns the substitution and the context
+(** [match_appsubterm pat c] returns the substitution and the context
corresponding to the first **closed** subterm of [c] matching [pat],
considering application contexts as well. It also returns a
continuation that looks for the next matching subterm.
It raises PatternMatchingFailure if no subterm matches the pattern *)
val match_appsubterm : constr_pattern -> constr -> subterm_matching_result
-(* [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
-val match_subterm_gen : bool (* true = with app context *) ->
+(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
+val match_subterm_gen : bool (** true = with app context *) ->
constr_pattern -> constr -> subterm_matching_result
-(* [is_matching_appsubterm pat c] tells if a subterm of [c] matches
+(** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
against [pat] taking partial subterms into consideration *)
val is_matching_appsubterm : ?closed:bool -> constr_pattern -> constr -> bool
-(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
+(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
up to conversion for constants in patterns *)
val is_matching_conv :
env -> Evd.evar_map -> constr_pattern -> constr -> bool
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 096c09b511..e3ab7d03e3 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.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
+ ***********************************************************************)
-(* $Id$ *)
+(** {% $ %}Id: namegen.mli 12549 2009-12-01 12:05:57Z herbelin {% $ %} *)
open Names
open Term
open Environ
-(**********************************************************************)
-(* Generating "intuitive" names from their type *)
+(*********************************************************************
+ Generating "intuitive" names from their type *)
val lowercase_first_char : identifier -> string
val sort_hdchar : sorts -> string
@@ -24,7 +24,7 @@ val named_hd : env -> types -> name -> name
val mkProd_name : env -> name * types * types -> types
val mkLambda_name : env -> name * types * constr -> constr
-(* Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
+(** Deprecated synonyms of [mkProd_name] and [mkLambda_name] *)
val prod_name : env -> name * types * types -> types
val lambda_name : env -> name * types * constr -> constr
@@ -38,32 +38,32 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types
val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
-(**********************************************************************)
-(* Fresh names *)
+(*********************************************************************
+ Fresh names *)
-(* Avoid clashing with a name of the given list *)
+(** Avoid clashing with a name of the given list *)
val next_ident_away : identifier -> identifier list -> identifier
-(* Avoid clashing with a name already used in current module *)
+(** Avoid clashing with a name already used in current module *)
val next_ident_away_in_goal : identifier -> identifier list -> identifier
-(* Avoid clashing with a name already used in current module *)
-(* but tolerate overwriting section variables, as in goals *)
+(** Avoid clashing with a name already used in current module
+ but tolerate overwriting section variables, as in goals *)
val next_global_ident_away : identifier -> identifier list -> identifier
-(* Avoid clashing with a constructor name already used in current module *)
+(** Avoid clashing with a constructor name already used in current module *)
val next_name_away_in_cases_pattern : name -> identifier list -> identifier
-val next_name_away : name -> identifier list -> identifier (* default is "H" *)
+val next_name_away : name -> identifier list -> identifier (** default is "H" *)
val next_name_away_with_default : string -> name -> identifier list ->
identifier
-(**********************************************************************)
-(* Making name distinct for displaying *)
+(*********************************************************************
+ Making name distinct for displaying *)
type renaming_flags =
- | RenamingForCasesPattern (* avoid only global constructors *)
- | RenamingForGoal (* avoid all globals (as in intro) *)
+ | RenamingForCasesPattern (** avoid only global constructors *)
+ | RenamingForGoal (** avoid all globals (as in intro) *)
| RenamingElsewhereFor of constr
val make_all_name_different : env -> env
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index e7460377b1..33105c3128 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.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 Pp
open Names
open Sign
@@ -18,14 +17,13 @@ open Libnames
open Nametab
open Rawterm
open Mod_subst
-(*i*)
-(* Pattern variables *)
+(** Pattern variables *)
type patvar_map = (patvar * constr) list
val pr_patvar : patvar -> std_ppcmds
-(* Patterns *)
+(** Patterns *)
type constr_pattern =
| PRef of global_reference
@@ -51,24 +49,24 @@ val subst_pattern : substitution -> constr_pattern -> constr_pattern
exception BoundPattern
-(* [head_pattern_bound t] extracts the head variable/constant of the
+(** [head_pattern_bound t] extracts the head variable/constant of the
type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly
if [t] is an abstraction *)
val head_pattern_bound : constr_pattern -> global_reference
-(* [head_of_constr_reference c] assumes [r] denotes a reference and
+(** [head_of_constr_reference c] assumes [r] denotes a reference and
returns its label; raises an anomaly otherwise *)
val head_of_constr_reference : Term.constr -> global_reference
-(* [pattern_of_constr c] translates a term [c] with metavariables into
+(** [pattern_of_constr c] translates a term [c] with metavariables into
a pattern; currently, no destructor (Cases, Fix, Cofix) and no
existential variable are allowed in [c] *)
val pattern_of_constr : Evd.evar_map -> constr -> named_context * constr_pattern
-(* [pattern_of_rawconstr l c] translates a term [c] with metavariables into
+(** [pattern_of_rawconstr l c] translates a term [c] with metavariables into
a pattern; variables bound in [l] are replaced by the pattern to which they
are bound *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index ca48f70211..9b6216a126 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.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 Pp
open Util
open Names
@@ -17,14 +16,13 @@ open Sign
open Environ
open Rawterm
open Inductiveops
-(*i*)
-(*s The type of errors raised by the pretyper *)
+(** {6 The type of errors raised by the pretyper } *)
type pretype_error =
- (* Old Case *)
+ (** Old Case *)
| CantFindCaseType of constr
- (* Unification *)
+ (** Unification *)
| OccurCheck of existential_key * constr
| NotClean of existential_key * constr * Evd.hole_kind
| UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
@@ -35,7 +33,7 @@ type pretype_error =
| CannotGeneralize of constr
| NoOccurrenceFound of constr * identifier option
| CannotFindWellTypedAbstraction of constr * constr list
- (* Pretyping *)
+ (** Pretyping *)
| VarNotFound of identifier
| UnexpectedType of constr * constr
| NotProduct of constr
@@ -44,7 +42,7 @@ exception PretypeError of env * pretype_error
val precatchable_exception : exn -> bool
-(* Presenting terms without solved evars *)
+(** Presenting terms without solved evars *)
val nf_evar : Evd.evar_map -> constr -> constr
val j_nf_evar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
val jl_nf_evar :
@@ -55,7 +53,7 @@ val tj_nf_evar :
Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
-(* Raising errors *)
+(** Raising errors *)
val error_actual_type_loc :
loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
@@ -87,7 +85,7 @@ val error_not_a_type_loc :
val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
-(*s Implicit arguments synthesis errors *)
+(** {6 Implicit arguments synthesis errors } *)
val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
@@ -105,12 +103,12 @@ val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -
val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
constr -> constr list -> 'b
-(*s Ml Case errors *)
+(** {6 Ml Case errors } *)
val error_cant_find_case_type_loc :
loc -> env -> Evd.evar_map -> constr -> 'b
-(*s Pretyping errors *)
+(** {6 Pretyping errors } *)
val error_unexpected_type_loc :
loc -> env -> Evd.evar_map -> constr -> constr -> 'b
@@ -118,6 +116,6 @@ val error_unexpected_type_loc :
val error_not_product_loc :
loc -> env -> Evd.evar_map -> constr -> 'b
-(*s Error in conversion from AST to rawterms *)
+(** {6 Error in conversion from AST to rawterms } *)
val error_var_not_found_loc : loc -> identifier -> 'b
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 75bd7874e7..f5601d6d65 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.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 Sign
open Term
@@ -16,9 +15,8 @@ open Environ
open Evd
open Rawterm
open Evarutil
-(*i*)
-(* An auxiliary function for searching for fixpoint guard indexes *)
+(** An auxiliary function for searching for fixpoint guard indexes *)
val search_guard :
Util.loc -> env -> int list list -> rec_declaration -> int array
@@ -33,10 +31,10 @@ sig
module Cases : Cases.S
- (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+ (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
val allow_anonymous_refs : bool ref
- (* Generic call to the interpreter from rawconstr to open_constr, leaving
+ (** Generic call to the interpreter from rawconstr to open_constr, leaving
unresolved holes as evars and returning the typing contexts of
these evars. Work as [understand_gen] for the rest. *)
@@ -46,9 +44,9 @@ sig
val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
evar_map ref -> env -> typing_constraint -> rawconstr -> constr
- (* More general entry point with evars from ltac *)
+ (** More general entry point with evars from ltac *)
- (* Generic call to the interpreter from rawconstr to constr, failing
+ (** Generic call to the interpreter from rawconstr to constr, failing
unresolved holes in the rawterm cannot be instantiated.
In [understand_ltac expand_evars sigma env ltac_env constraint c],
@@ -63,29 +61,29 @@ sig
bool -> evar_map -> env -> var_map * unbound_ltac_var_map ->
typing_constraint -> rawconstr -> evar_map * constr
- (* Standard call to get a constr from a rawconstr, resolving implicit args *)
+ (** Standard call to get a constr from a rawconstr, resolving implicit args *)
val understand : evar_map -> env -> ?expected_type:Term.types ->
rawconstr -> constr
- (* Idem but the rawconstr is intended to be a type *)
+ (** Idem but the rawconstr is intended to be a type *)
val understand_type : evar_map -> env -> rawconstr -> constr
- (* A generalization of the two previous case *)
+ (** A generalization of the two previous case *)
val understand_gen : typing_constraint -> evar_map -> env ->
rawconstr -> constr
- (* Idem but returns the judgment of the understood term *)
+ (** Idem but returns the judgment of the understood term *)
val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
- (* Idem but do not fail on unresolved evars *)
+ (** Idem but do not fail on unresolved evars *)
val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment
- (*i*)
- (* Internal of Pretyping...
+ (**/**)
+ (** Internal of Pretyping...
*)
val pretype :
type_constraint -> env -> evar_map ref ->
@@ -102,14 +100,14 @@ sig
var_map * (identifier * identifier option) list ->
typing_constraint -> rawconstr -> constr
- (*i*)
+ (**/**)
end
module Pretyping_F (C : Coercion.S) : S
module Default : S
-(* To embed constr in rawconstr *)
+(** To embed constr in rawconstr *)
val constr_in : constr -> Dyn.t
val constr_out : Dyn.t -> constr
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 74a0d7d8ec..954890d894 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -1,23 +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 Nametab
open Term
open Libnames
open Libobject
open Library
-(*i*)
-(*s A structure S is a non recursive inductive type with a single
+(** {6 Sect } *)
+(** A structure S is a non recursive inductive type with a single
constructor (the name of which defaults to Build_S) *)
type struc_typ = {
@@ -29,34 +28,35 @@ type struc_typ = {
val declare_structure :
inductive * constructor * (name * bool) list * constant option list -> unit
-(* [lookup_structure isp] returns the struc_typ associated to the
+(** [lookup_structure isp] returns the struc_typ associated to the
inductive path [isp] if it corresponds to a structure, otherwise
it fails with [Not_found] *)
val lookup_structure : inductive -> struc_typ
-(* [lookup_projections isp] returns the projections associated to the
+(** [lookup_projections isp] returns the projections associated to the
inductive path [isp] if it corresponds to a structure, otherwise
it fails with [Not_found] *)
val lookup_projections : inductive -> constant option list
-(* raise [Not_found] if not a projection *)
+(** raise [Not_found] if not a projection *)
val find_projection_nparams : global_reference -> int
-(* raise [Not_found] if not a projection *)
+(** raise [Not_found] if not a projection *)
val find_projection : global_reference -> struc_typ
-(* we keep an index (dnet) of record's arguments + fields
+(** we keep an index (dnet) of record's arguments + fields
(=methods). Here is how to declare them: *)
val declare_method :
global_reference -> Evd.evar -> Evd.evar_map -> unit
- (* and here is how to search for methods matched by a given term: *)
+ (** and here is how to search for methods matched by a given term: *)
val methods_matching : constr ->
((global_reference*Evd.evar*Evd.evar_map) *
(constr*existential_key)*Termops.subst) list
-(*s A canonical structure declares "canonical" conversion hints between *)
-(* the effective components of a structure and the projections of the *)
-(* structure *)
+(** {6 Sect } *)
+(** A canonical structure declares "canonical" conversion hints between
+ the effective components of a structure and the projections of the
+ structure *)
type cs_pattern =
Const_cs of global_reference
@@ -66,11 +66,11 @@ type cs_pattern =
type obj_typ = {
o_DEF : constr;
- o_INJ : int; (* position of trivial argument *)
- o_TABS : constr list; (* ordered *)
- o_TPARAMS : constr list; (* ordered *)
+ o_INJ : int; (** position of trivial argument *)
+ o_TABS : constr list; (** ordered *)
+ o_TPARAMS : constr list; (** ordered *)
o_NPARAMS : int;
- o_TCOMPS : constr list } (* ordered *)
+ o_TCOMPS : constr list } (** ordered *)
val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 0b9e69d95b..84bd20135f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -1,28 +1,26 @@
-(************************************************************************)
-(* 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
open Evd
open Environ
open Closure
-(*i*)
-(* Reduction Functions. *)
+(** Reduction Functions. *)
exception Elimconst
-(************************************************************************)
-(*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 *)
@@ -67,13 +65,13 @@ type contextual_state_reduction_function =
type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
-(* Removes cast and put into applicative form *)
+(** Removes cast and put into applicative form *)
val whd_stack : local_stack_reduction_function
-(* For compatibility: alias for whd\_stack *)
+(** For compatibility: alias for whd\_stack *)
val whd_castapp_stack : local_stack_reduction_function
-(*s Reduction Function Operators *)
+(** {6 Reduction Function Operators } *)
val strong : reduction_function -> reduction_function
val local_strong : local_reduction_function -> local_reduction_function
@@ -84,17 +82,19 @@ val stack_reduction_of_reduction :
i*)
val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a
-(*s Generic Optimized Reduction Function using Closures *)
+(** {6 Generic Optimized Reduction Function using Closures } *)
val clos_norm_flags : Closure.RedFlags.reds -> reduction_function
-(* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *)
+
+(** Same as [(strong whd_beta[delta][iota])], but much faster on big terms *)
val nf_beta : local_reduction_function
val nf_betaiota : local_reduction_function
val nf_betadeltaiota : reduction_function
val nf_evar : evar_map -> constr -> constr
val nf_betaiota_preserving_vm_cast : reduction_function
-(* Lazy strategy, weak head reduction *)
+
+(** Lazy strategy, weak head reduction *)
val whd_evar : evar_map -> constr -> constr
val whd_beta : local_reduction_function
val whd_betaiota : local_reduction_function
@@ -120,7 +120,7 @@ val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
val whd_betaetalet_state : local_state_reduction_function
val whd_betalet_state : local_state_reduction_function
-(*s Head normal forms *)
+(** {6 Head normal forms } *)
val whd_delta_stack : stack_reduction_function
val whd_delta_state : state_reduction_function
@@ -138,7 +138,7 @@ val whd_betadeltaiotaeta : reduction_function
val whd_eta : constr -> constr
val whd_zeta : constr -> constr
-(* Various reduction functions *)
+(** Various reduction functions *)
val safe_evar_value : evar_map -> existential -> constr option
@@ -163,11 +163,11 @@ val decomp_sort : env -> evar_map -> types -> sorts
val is_sort : env -> evar_map -> types -> bool
type 'a miota_args = {
- mP : constr; (* the result type *)
- mconstr : constr; (* the constructor *)
- mci : case_info; (* special info to re-build pattern *)
- mcargs : 'a list; (* the constructor's arguments *)
- mlf : 'a array } (* the branch code vector *)
+ mP : constr; (** the result type *)
+ mconstr : constr; (** the constructor *)
+ mci : case_info; (** special info to re-build pattern *)
+ mcargs : 'a list; (** the constructor's arguments *)
+ mlf : 'a array } (** the branch code vector *)
val reducible_mind_case : constr -> bool
val reduce_mind_case : constr miota_args -> constr
@@ -177,7 +177,7 @@ val is_arity : env -> evar_map -> constr -> bool
val whd_programs : reduction_function
-(* [reduce_fix redfun fix stk] contracts [fix stk] if it is actually
+(** [reduce_fix redfun fix stk] contracts [fix stk] if it is actually
reducible; the structural argument is reduced by [redfun] *)
type fix_reduction_result = NotReducible | Reduced of state
@@ -186,10 +186,10 @@ val fix_recarg : fixpoint -> constr stack -> (int * constr) option
val reduce_fix : local_state_reduction_function -> evar_map -> fixpoint
-> constr stack -> fix_reduction_result
-(*s Querying the kernel conversion oracle: opaque/transparent constants *)
+(** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
val is_transparent : 'a tableKey -> bool
-(*s Conversion Functions (uses closures, lazy strategy) *)
+(** {6 Conversion Functions (uses closures, lazy strategy) } *)
type conversion_test = constraints -> constraints
@@ -206,18 +206,18 @@ val is_trans_conv : transparent_state -> env -> evar_map -> constr -> constr ->
val is_trans_conv_leq : transparent_state -> env -> evar_map -> constr -> constr -> bool
val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr -> constr -> bool
-(*s Special-Purpose Reduction Functions *)
+(** {6 Special-Purpose Reduction Functions } *)
val whd_meta : (metavariable * constr) list -> constr -> constr
val plain_instance : (metavariable * constr) list -> constr -> constr
val instance :evar_map -> (metavariable * constr) list -> constr -> constr
val head_unfold_under_prod : transparent_state -> reduction_function
-(*s Heuristic for Conversion with Evar *)
+(** {6 Heuristic for Conversion with Evar } *)
val whd_betaiota_deltazeta_for_iota_state : state_reduction_function
-(*s Meta-related reduction functions *)
+(** {6 Meta-related reduction functions } *)
val meta_instance : evar_map -> constr freelisted -> constr
val nf_meta : evar_map -> constr -> constr
val meta_reducible_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 8576d5baa3..3c68f850b0 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.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 Names
open Term
open Evd
open Environ
-(*i*)
-(* This family of functions assumes its constr argument is known to be
+(** This family of functions assumes its constr argument is known to be
well-typable. It does not type-check, just recompute the type
without any costly verifications. On non well-typable terms, it
either produces a wrong result or raise an anomaly. Use with care.
@@ -25,10 +23,10 @@ val get_type_of : ?refresh:bool -> env -> evar_map -> constr -> types
val get_sort_of : env -> evar_map -> types -> sorts
val get_sort_family_of : env -> evar_map -> types -> sorts_family
-(* Makes an assumption from a constr *)
+(** Makes an assumption from a constr *)
val get_assumption_of : env -> evar_map -> constr -> types
-(* Makes an unsafe judgment from a constr *)
+(** Makes an unsafe judgment from a constr *)
val get_judgment_of : env -> evar_map -> constr -> unsafe_judgment
val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 2bba87a75e..84cff15b63 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.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 Environ
@@ -18,16 +17,15 @@ open Closure
open Rawterm
open Termops
open Pattern
-(*i*)
type reduction_tactic_error =
InvalidAbstraction of env * constr * (env * Type_errors.type_error)
exception ReductionTacticError of reduction_tactic_error
-(*s Reduction functions associated to tactics. \label{tacred} *)
+(** {6 Reduction functions associated to tactics. {% \label{%}tacred{% }%} } *)
-(* Evaluable global reference *)
+(** Evaluable global reference *)
val is_evaluable : Environ.env -> evaluable_global_reference -> bool
@@ -41,51 +39,52 @@ val global_of_evaluable_reference :
exception Redelimination
-(* Red (raise user error if nothing reducible) *)
+(** Red (raise user error if nothing reducible) *)
val red_product : reduction_function
-(* Red (raise Redelimination if nothing reducible) *)
+(** Red (raise Redelimination if nothing reducible) *)
val try_red_product : reduction_function
-(* Simpl *)
+(** Simpl *)
val simpl : reduction_function
-(* Simpl only at the head *)
+(** Simpl only at the head *)
val whd_simpl : reduction_function
-(* Hnf: like whd_simpl but force delta-reduction of constants that do
+(** Hnf: like whd_simpl but force delta-reduction of constants that do
not immediately hide a non reducible fix or cofix *)
val hnf_constr : reduction_function
-(* Unfold *)
+(** Unfold *)
val unfoldn :
(occurrences * evaluable_global_reference) list -> reduction_function
-(* Fold *)
+(** Fold *)
val fold_commands : constr list -> reduction_function
-(* Pattern *)
+(** Pattern *)
val pattern_occs : (occurrences * constr) list -> reduction_function
-(* Rem: Lazy strategies are defined in Reduction *)
-(* Call by value strategy (uses Closures) *)
+(** Rem: Lazy strategies are defined in Reduction *)
+
+(** Call by value strategy (uses Closures) *)
val cbv_norm_flags : Closure.RedFlags.reds -> reduction_function
val cbv_beta : local_reduction_function
val cbv_betaiota : local_reduction_function
val cbv_betadeltaiota : reduction_function
- val compute : reduction_function (* = [cbv_betadeltaiota] *)
+ val compute : reduction_function (** = [cbv_betadeltaiota] *)
-(* [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
+(** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
with [I] an inductive definition;
returns [I] and [t'] or fails with a user error *)
val reduce_to_atomic_ind : env -> evar_map -> types -> inductive * types
-(* [reduce_to_quantified_ind env sigma t] puts [t] in the form
+(** [reduce_to_quantified_ind env sigma t] puts [t] in the form
[t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition;
returns [I] and [t'] or fails with a user error *)
val reduce_to_quantified_ind : env -> evar_map -> types -> inductive * types
-(* [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
+(** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form
[t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *)
val reduce_to_quantified_ref :
env -> evar_map -> Libnames.global_reference -> types -> types
diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index 0e7fdb82a7..7623fcd68d 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.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
+ ***********************************************************************)
-(* $Id:$ *)
+(** {% $ %}Id:{% $ %} *)
-(*i*)
open Term
open Sign
open Libnames
open Mod_subst
-(*i*)
-(* Dnets on constr terms.
+(** Dnets on constr terms.
An instantiation of Dnet on (an approximation of) constr. It
associates a term (possibly with Evar) with an
@@ -33,25 +31,25 @@ open Mod_subst
See lib/dnet.mli for more details.
*)
-(* Identifiers to store (right hand side of the association) *)
+(** Identifiers to store (right hand side of the association) *)
module type IDENT = sig
type t
val compare : t -> t -> int
- (* how to substitute them for storage *)
+ (** how to substitute them for storage *)
val subst : substitution -> t -> t
- (* how to recover the term from the identifier *)
+ (** how to recover the term from the identifier *)
val constr_of : t -> constr
end
-(* Options : *)
+(** Options : *)
module type OPT = sig
- (* pre-treatment to terms before adding or searching *)
+ (** pre-treatment to terms before adding or searching *)
val reduce : constr -> constr
- (* direction of post-filtering w.r.t sort subtyping :
+ (** direction of post-filtering w.r.t sort subtyping :
- true means query <= terms in the structure
- false means terms <= query
*)
@@ -63,17 +61,17 @@ sig
type t
type ident
- (* results of filtering : identifier, a context (term with Evar
+ (** results of filtering : identifier, a context (term with Evar
hole) and the substitution in that context*)
type result = ident * (constr*existential_key) * Termops.subst
val empty : t
- (* [add c i dn] adds the binding [(c,i)] to [dn]. [c] can be a
+ (** [add c i dn] adds the binding [(c,i)] to [dn]. [c] can be a
closed term or a pattern (with untyped Evars). No Metas accepted *)
val add : constr -> ident -> t -> t
- (* merge of dnets. Faster than re-adding all terms *)
+ (** merge of dnets. Faster than re-adding all terms *)
val union : t -> t -> t
val subst : substitution -> t -> t
@@ -82,25 +80,25 @@ sig
* High-level primitives describing specific search problems
*)
- (* [search_pattern dn c] returns all terms/patterns in dn
+ (** [search_pattern dn c] returns all terms/patterns in dn
matching/matched by c *)
val search_pattern : t -> constr -> result list
- (* [search_concl dn c] returns all matches under products and
+ (** [search_concl dn c] returns all matches under products and
letins, i.e. it finds subterms whose conclusion matches c. The
complexity depends only on c ! *)
val search_concl : t -> constr -> result list
- (* [search_head_concl dn c] matches under products and applications
+ (** [search_head_concl dn c] matches under products and applications
heads. Finds terms of the form [forall H_1...H_n, C t_1...t_n]
where C matches c *)
val search_head_concl : t -> constr -> result list
- (* [search_eq_concl dn eq c] searches terms of the form [forall
+ (** [search_eq_concl dn eq c] searches terms of the form [forall
H1...Hn, eq _ X1 X2] where either X1 or X2 matches c *)
val search_eq_concl : t -> constr -> constr -> result list
- (* [find_all dn] returns all idents contained in dn *)
+ (** [find_all dn] returns all idents contained in dn *)
val find_all : t -> ident list
val map : (ident -> ident) -> t -> t
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 59f7750d3f..57b5bd5815 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.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*)
@@ -15,7 +15,7 @@ open Term
open Sign
open Environ
-(* Universes *)
+(** Universes *)
val new_univ : unit -> Univ.universe
val new_sort_in_family : sorts_family -> sorts
val new_Type : unit -> types
@@ -23,10 +23,11 @@ val new_Type_sort : unit -> sorts
val refresh_universes : types -> types
val refresh_universes_strict : types -> types
-(* printers *)
+(** printers *)
val print_sort : sorts -> std_ppcmds
val pr_sort_family : sorts_family -> std_ppcmds
-(* debug printer: do not use to display terms to the casual user... *)
+
+(** debug printer: do not use to display terms to the casual user... *)
val set_print_constr : (env -> constr -> std_ppcmds) -> unit
val print_constr : constr -> std_ppcmds
val print_constr_env : env -> constr -> std_ppcmds
@@ -35,19 +36,19 @@ val pr_rel_decl : env -> rel_declaration -> std_ppcmds
val print_rel_context : env -> std_ppcmds
val print_env : env -> std_ppcmds
-(* about contexts *)
+(** about contexts *)
val push_rel_assum : name * types -> env -> env
val push_rels_assum : (name * types) list -> env -> env
val push_named_rec_types : name array * types array * 'a -> env -> env
val lookup_rel_id : identifier -> rel_context -> int * constr option * types
-(* builds argument lists matching a block of binders or a context *)
+(** builds argument lists matching a block of binders or a context *)
val rel_vect : int -> int -> constr array
val rel_list : int -> int -> constr list
val extended_rel_list : int -> rel_context -> constr list
val extended_rel_vect : int -> rel_context -> constr array
-(* iterators/destructors on terms *)
+(** iterators/destructors on terms *)
val mkProd_or_LetIn : rel_declaration -> types -> types
val mkProd_wo_LetIn : rel_declaration -> types -> types
val it_mkProd : init:types -> (name * types) list -> types
@@ -62,8 +63,8 @@ val it_mkNamedLambda_or_LetIn : init:constr -> named_context -> constr
val it_named_context_quantifier :
(named_declaration -> 'a -> 'a) -> init:'a -> named_context -> 'a
-(**********************************************************************)
-(* Generic iterators on constr *)
+(*********************************************************************
+ Generic iterators on constr *)
val map_constr_with_named_binders :
(name -> 'a -> 'a) ->
@@ -76,7 +77,7 @@ val map_constr_with_full_binders :
(rel_declaration -> 'a -> 'a) ->
('a -> constr -> constr) -> 'a -> constr -> constr
-(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+(** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
subterms of [c] starting from [acc] and proceeding from left to
right according to the usual representation of the constructions as
[fold_constr] but it carries an extra data [n] (typically a lift
@@ -94,7 +95,7 @@ val iter_constr_with_full_binders :
val strip_head_cast : constr -> constr
-(* occur checks *)
+(** occur checks *)
exception Occur
val occur_meta : types -> bool
val occur_existential : types -> bool
@@ -109,56 +110,57 @@ val free_rels : constr -> Intset.t
val dependent : constr -> constr -> bool
val dependent_no_evar : constr -> constr -> bool
val collect_metas : constr -> int list
-val occur_term : constr -> constr -> bool (* Synonymous
- of dependent *)
-(* Substitution of metavariables *)
+val occur_term : constr -> constr -> bool (** Synonymous
+ of dependent
+ Substitution of metavariables *)
type meta_value_map = (metavariable * constr) list
val subst_meta : meta_value_map -> constr -> constr
-(* Type assignment for metavariables *)
+(** Type assignment for metavariables *)
type meta_type_map = (metavariable * types) list
-(* [pop c] lifts by -1 the positive indexes in [c] *)
+(** [pop c] lifts by -1 the positive indexes in [c] *)
val pop : constr -> constr
-(*s Substitution of an arbitrary large term. Uses equality modulo
+(** {6 Sect } *)
+(** Substitution of an arbitrary large term. Uses equality modulo
reduction of let *)
-(* [subst_term_gen eq d c] replaces [Rel 1] by [d] in [c] using [eq]
+(** [subst_term_gen eq d c] replaces [Rel 1] by [d] in [c] using [eq]
as equality *)
val subst_term_gen :
(constr -> constr -> bool) -> constr -> constr -> constr
-(* [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
+(** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq]
as equality *)
val replace_term_gen :
(constr -> constr -> bool) ->
constr -> constr -> constr -> constr
-(* [subst_term d c] replaces [Rel 1] by [d] in [c] *)
+(** [subst_term d c] replaces [Rel 1] by [d] in [c] *)
val subst_term : constr -> constr -> constr
-(* [replace_term d e c] replaces [d] by [e] in [c] *)
+(** [replace_term d e c] replaces [d] by [e] in [c] *)
val replace_term : constr -> constr -> constr -> constr
-(* In occurrences sets, false = everywhere except and true = nowhere except *)
+(** In occurrences sets, false = everywhere except and true = nowhere except *)
type occurrences = bool * int list
val all_occurrences : occurrences
val no_occurrences_in_set : occurrences
-(* [subst_term_occ_gen occl n c d] replaces occurrences of [c] at
+(** [subst_term_occ_gen occl n c d] replaces occurrences of [c] at
positions [occl], counting from [n], by [Rel 1] in [d] *)
val subst_term_occ_gen :
occurrences -> int -> constr -> types -> int * types
-(* [subst_term_occ occl c d] replaces occurrences of [c] at
+(** [subst_term_occ occl c d] replaces occurrences of [c] at
positions [occl] by [Rel 1] in [d] (see also Note OCC) *)
val subst_term_occ : occurrences -> constr -> constr -> constr
-(* [subst_term_occ_decl occl c decl] replaces occurrences of [c] at
+(** [subst_term_occ_decl occl c decl] replaces occurrences of [c] at
positions [occl] by [Rel 1] in [decl] *)
-type hyp_location_flag = (* To distinguish body and type of local defs *)
+type hyp_location_flag = (** To distinguish body and type of local defs *)
| InHyp
| InHypTypeOnly
| InHypValueOnly
@@ -169,7 +171,7 @@ val subst_term_occ_decl :
val error_invalid_occurrence : int list -> 'a
-(* Alternative term equalities *)
+(** Alternative term equalities *)
val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool
val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) ->
Reduction.conv_pb -> constr -> constr -> bool
@@ -181,7 +183,7 @@ val eta_eq_constr : constr -> constr -> bool
exception CannotFilter
-(* Lightweight first-order filtering procedure. Unification
+(** Lightweight first-order filtering procedure. Unification
variables ar represented by (untyped) Evars.
[filtering c1 c2] returns the substitution n'th evar ->
(context,term), or raises [CannotFilter].
@@ -193,10 +195,10 @@ val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
val decompose_prod_letin : constr -> int * rel_context * constr
val align_prod_letin : constr -> constr -> rel_context * constr
-(* Get the last arg of a constr intended to be an application *)
+(** Get the last arg of a constr intended to be an application *)
val last_arg : constr -> constr
-(* name contexts *)
+(** name contexts *)
type names_context = name list
val add_name : name -> names_context -> names_context
val lookup_name_of_rel : int -> names_context -> name
@@ -209,16 +211,16 @@ val names_of_rel_context : env -> names_context
val context_chop : int -> rel_context -> (rel_context*rel_context)
-(* Set of local names *)
+(** Set of local names *)
val vars_of_env: env -> Idset.t
val add_vname : Idset.t -> name -> Idset.t
-(* other signature iterators *)
+(** other signature iterators *)
val process_rel_context : (rel_declaration -> env -> env) -> env -> env
val assums_of_rel_context : rel_context -> (name * constr) list
val lift_rel_context : int -> rel_context -> rel_context
val substl_rel_context : constr list -> rel_context -> rel_context
-val smash_rel_context : rel_context -> rel_context (* expand lets in context *)
+val smash_rel_context : rel_context -> rel_context (** expand lets in context *)
val adjust_subst_to_rel_context : rel_context -> constr list -> constr list
val map_rel_context_in_env :
(env -> constr -> constr) -> env -> rel_context -> rel_context
@@ -232,18 +234,18 @@ val mem_named_context : identifier -> named_context -> bool
val global_vars : env -> constr -> identifier list
val global_vars_set_of_decl : env -> named_declaration -> Idset.t
-(* Gives an ordered list of hypotheses, closed by dependencies,
+(** Gives an ordered list of hypotheses, closed by dependencies,
containing a given set *)
val dependency_closure : env -> named_context -> Idset.t -> identifier list
-(* Test if an identifier is the basename of a global reference *)
+(** Test if an identifier is the basename of a global reference *)
val is_section_variable : identifier -> bool
val isGlobalRef : constr -> bool
val has_polymorphic_type : constant -> bool
-(* Combinators on judgments *)
+(** Combinators on judgments *)
val on_judgment : (types -> types) -> unsafe_judgment -> unsafe_judgment
val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index e53be5c0bf..c816f2e9c9 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.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 Libnames
open Decl_kinds
@@ -20,23 +19,22 @@ open Nametab
open Mod_subst
open Topconstr
open Util
-(*i*)
-(* This module defines type-classes *)
+(** This module defines type-classes *)
type typeclass = {
- (* The class implementation: a record parameterized by the context with defs in it or a definition if
+ (** The class implementation: a record parameterized by the context with defs in it or a definition if
the class is a singleton. This acts as the class' global identifier. *)
cl_impl : global_reference;
- (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
+ (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
The boolean indicates if the typeclass argument is a direct superclass and the global reference
gives a direct link to the class itself. *)
cl_context : (global_reference * bool) option list * rel_context;
- (* Context of definitions and properties on defs, will not be shared *)
+ (** Context of definitions and properties on defs, will not be shared *)
cl_props : rel_context;
- (* The methods implementations of the typeclass as projections. Some may be undefinable due to
+ (** The methods implementations of the typeclass as projections. Some may be undefinable due to
sorting restrictions. *)
cl_projs : (identifier * constant option) list;
}
@@ -56,13 +54,13 @@ val add_inductive_class : inductive -> unit
val new_instance : typeclass -> int option -> bool -> global_reference -> instance
val add_instance : instance -> unit
-val class_info : global_reference -> typeclass (* raises a UserError if not a class *)
+val class_info : global_reference -> typeclass (** raises a UserError if not a class *)
-(* These raise a UserError if not a class. *)
+(** These raise a UserError if not a class. *)
val dest_class_app : env -> constr -> typeclass * constr list
-(* Just return None if not a class *)
+(** Just return None if not a class *)
val class_of_constr : constr -> typeclass option
val instance_impl : instance -> global_reference
@@ -72,7 +70,7 @@ val is_instance : global_reference -> bool
val is_implicit_arg : hole_kind -> bool
-(* Returns the term and type for the given instance of the parameters and fields
+(** Returns the term and type for the given instance of the parameters and fields
of the type class. *)
val instance_constructor : typeclass -> constr list -> constr * types
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 7fd04e225d..24a19a0e37 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.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 Decl_kinds
open Term
@@ -20,16 +19,15 @@ open Mod_subst
open Topconstr
open Util
open Libnames
-(*i*)
type contexts = Parameters | Properties
type typeclass_error =
| NotAClass of constr
- | UnboundMethod of global_reference * identifier located (* Class name, method *)
+ | UnboundMethod of global_reference * identifier located (** Class name, method *)
| NoInstance of identifier located * constr list
| UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option
- | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
+ | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
exception TypeClassError of env * typeclass_error
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index e3b3e94825..c20fd9453a 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -1,31 +1,31 @@
-(************************************************************************)
-(* 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 Evd
-(*i*)
-(* This module provides the typing machine with existential variables
+(** This module provides the typing machine with existential variables
(but without universes). *)
-(* Typecheck a term and return its type *)
+(** Typecheck a term and return its type *)
val type_of : env -> evar_map -> constr -> types
-(* Typecheck a type and return its sort *)
+
+(** Typecheck a type and return its sort *)
val sort_of : env -> evar_map -> types -> sorts
-(* Typecheck a term has a given type (assuming the type is OK) *)
+
+(** Typecheck a term has a given type (assuming the type is OK) *)
val check : env -> evar_map -> constr -> types -> unit
-(* Returns the instantiated type of a metavariable *)
+(** Returns the instantiated type of a metavariable *)
val meta_type : evar_map -> metavariable -> types
-(* Solve existential variables using typing *)
+(** Solve existential variables using typing *)
val solve_evars : env -> evar_map -> constr -> constr
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index cc62a9bb81..13042180a8 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.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 Term
open Environ
open Evd
-(*i*)
type unify_flags = {
modulo_conv_on_closed_terms : Names.transparent_state option;
@@ -25,11 +23,11 @@ type unify_flags = {
val default_unify_flags : unify_flags
val default_no_delta_unify_flags : unify_flags
-(* The "unique" unification fonction *)
+(** The "unique" unification fonction *)
val w_unify :
bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map
-(* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
+(** [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
subterm of [t]. Constraints are added to [m] and the matched
subterm of [t] is also returned. *)
val w_unify_to_subterm :
@@ -40,15 +38,15 @@ val w_unify_to_subterm_all :
val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map
-(* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type
+(** [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type
[ctyp] so that its gets type [typ]; [typ] may contain metavariables *)
val w_coerce_to_type : env -> evar_map -> constr -> types -> types ->
evar_map * constr
(*i This should be in another module i*)
-(* [abstract_list_all env evd t c l] *)
-(* abstracts the terms in l over c to get a term of type t *)
-(* (exported for inv.ml) *)
+(** [abstract_list_all env evd t c l]
+ abstracts the terms in l over c to get a term of type t
+ (exported for inv.ml) *)
val abstract_list_all :
env -> evar_map -> constr -> constr -> constr list -> constr
diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli
index 2ea94bfb04..da9e7cf1e5 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.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*)
open Names
open Term
open Environ
open Reduction
-(*i*)
-(*s Reduction functions *)
+(** {6 Reduction functions } *)
val cbv_vm : env -> constr -> types -> constr
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-08 17:38:07 +0000