diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 96 |
1 files changed, 48 insertions, 48 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index f895ead42..2601d44f7 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 |