diff options
Diffstat (limited to 'pretyping/pretyping.mli')
| -rw-r--r-- | pretyping/pretyping.mli | 44 |
1 files changed, 21 insertions, 23 deletions
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 75bd7874e..f5601d6d6 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 |