diff options
-rw-r--r-- | pretyping/evarutil.mli | 34 | ||||
-rw-r--r-- | pretyping/glob_term.mli | 13 |
2 files changed, 22 insertions, 25 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 35932bb8e..d3a2452de 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -15,10 +15,9 @@ open Evd open Environ open Reductionops -(** {6 This modules provides useful functions for unification modulo evars } *) +(** {5 This modules provides useful functions for unification modulo evars } *) -(********************************************************** - Metas *) +(** {6 Metas} *) (** [new_meta] is a generator of unique meta variables *) val new_meta : unit -> metavariable @@ -27,8 +26,7 @@ val mk_new_meta : unit -> constr (** [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 *) +(** {6 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 @@ -47,8 +45,7 @@ val new_evar_instance : val make_pure_subst : evar_info -> constr array -> (identifier * constr) list -(********************************************************** - Instantiate evars *) +(** {6 Instantiate evars} *) (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open @@ -56,8 +53,7 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list 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... *) +(** {6 Evars/Metas switching...} *) (** [evars_to_metas] generates new metavariables for each non dependent existential and performs the replacement in the given constr; it also @@ -66,10 +62,9 @@ val evars_to_metas : evar_map -> open_constr -> (evar_map * constr) val non_instantiated : evar_map -> (evar * evar_info) list -(********************************************************** - Unification utils *) +(** {6 Unification utils} *) -(** [head_evar c} returns the head evar of [c] if any *) +(** [head_evar c] returns the head evar of [c] if any *) exception NoHeadEvar val head_evar : constr -> existential_key (** may raise NoHeadEvar *) @@ -105,8 +100,7 @@ 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 *) +(** {6 Value/Type constraints} *) val judge_of_new_Type : unit -> unsafe_judgment @@ -166,16 +160,14 @@ val flush_and_check_evars : evar_map -> constr -> constr their representative that is most ancient in the context *) val expand_vars_in_term : env -> constr -> constr -(******************************************************************** - debug pretty-printer: *) +(** {6 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 *) +(** {6 Removing hyps in evars'context} +raise OccurHypInSimpleClause if the removal breaks dependencies *) type clear_dependency_error = | OccurHypInSimpleClause of identifier option @@ -183,14 +175,14 @@ type clear_dependency_error = exception ClearDependencyError of identifier * clear_dependency_error -(* spiwack: marks an evar that has been "defined" by clear. +(* spiwack: marks an evar that has been "defined" by clear. used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) val cleared : bool Store.Field.t val clear_hyps_in_evi : evar_map ref -> named_context_val -> types -> identifier list -> named_context_val * types -val push_rel_context_to_named_context : Environ.env -> types -> +val push_rel_context_to_named_context : Environ.env -> types -> named_context_val * types * constr list val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli index 4e11221d8..9649ad2c0 100644 --- a/pretyping/glob_term.mli +++ b/pretyping/glob_term.mli @@ -21,11 +21,11 @@ open Nametab (** The kind of patterns that occurs in "match ... with ... end" - locs here refers to the ident's location, not whole pat the last - argument of PatCstr is a possible alias ident for the pattern *) + locs here refers to the ident's location, not whole pat *) type cases_pattern = | PatVar of loc * name - | PatCstr of loc * constructor * cases_pattern list * name + | PatCstr of loc * constructor * cases_pattern list * name + (** [PatCstr(p,C,l,x)] = "|'C' 'l' as 'x'" *) val cases_pattern_loc : cases_pattern -> loc @@ -60,6 +60,9 @@ type glob_constr = | GProd of loc * name * binding_kind * glob_constr * glob_constr | GLetIn of loc * name * glob_constr * glob_constr | GCases of loc * case_style * glob_constr option * tomatch_tuples * cases_clauses + (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in + [MatchStyle]) *) + | GLetTuple of loc * name list * (name * glob_constr option) * glob_constr * glob_constr | GIf of loc * glob_constr * (name * glob_constr option) * glob_constr * glob_constr @@ -80,12 +83,15 @@ and fix_kind = and predicate_pattern = name * (loc * inductive * int * name list) option + (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)], [k] + is the number of parameter of [I]. *) and tomatch_tuple = (glob_constr * predicate_pattern) and tomatch_tuples = tomatch_tuple list and cases_clause = (loc * identifier list * cases_pattern list * glob_constr) +(** [(p,il,cl,t)] = "|'cl' as 'il' => 't'" *) and cases_clauses = cases_clause list @@ -113,7 +119,6 @@ val loc_of_glob_constr : glob_constr -> loc Take the current alias as parameter, @raise Not_found if translation is impossible *) - val cases_pattern_of_glob_constr : name -> glob_constr -> cases_pattern val glob_constr_of_closed_cases_pattern : cases_pattern -> name * glob_constr |