diff options
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/evarutil.ml | 5 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 7 | ||||
-rw-r--r-- | pretyping/evd.ml | 29 | ||||
-rw-r--r-- | pretyping/evd.mli | 7 |
4 files changed, 12 insertions, 36 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d286b98e8..0b8cbff36 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -838,3 +838,8 @@ let subterm_source evk (loc,k) = | Evar_kinds.SubEvar (evk) -> evk | _ -> evk in (loc,Evar_kinds.SubEvar evk) + + +(** Term exploration up to isntantiation. *) +let kind_of_term_upto sigma t = + Constr.kind (Reductionops.whd_evar sigma t) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f89266a60..92a3984ba 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -199,6 +199,13 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr) exception Uninstantiated_evar of existential_key val flush_and_check_evars : evar_map -> constr -> constr +(** {6 Term manipulation up to instantiation} *) + +(** Like {!Constr.kind} except that [kind_of_term sigma t] exposes [t] + as an evar [e] only if [e] is uninstantiated in [sigma]. Otherwise the + value of [e] in [sigma] is (recursively) used. *) +val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term + (** {6 debug pretty-printer:} *) val pr_tycon : env -> type_constraint -> Pp.std_ppcmds diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 4e38bd4e6..454c51195 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -568,14 +568,6 @@ type evar_map = { (*** Lifting primitive from Evar.Map. ***) -(* HH: The progress tactical now uses this function. *) -let progress_evar_map d1 d2 = - let is_new k v = - assert (v.evar_body == Evar_empty); - EvMap.mem k d2.defn_evars - in - not (d1 == d2) && EvMap.exists is_new d1.undf_evars - let add_name_newly_undefined naming evk evi (evtoid,idtoev) = let id = match naming with | Misctypes.IntroAnonymous -> @@ -1303,27 +1295,6 @@ let e_eq_constr_univs evdref t u = let eq_constr_univs_test evd t u = snd (eq_constr_univs evd t u) -let eq_named_context_val d ctx1 ctx2 = - ctx1 == ctx2 || - let c1 = named_context_of_val ctx1 and c2 = named_context_of_val ctx2 in - let eq_named_declaration (i1, c1, t1) (i2, c2, t2) = - Id.equal i1 i2 && Option.equal (eq_constr_univs_test d) c1 c2 - && (eq_constr_univs_test d) t1 t2 - in List.equal eq_named_declaration c1 c2 - -let eq_evar_body d b1 b2 = match b1, b2 with -| Evar_empty, Evar_empty -> true -| Evar_defined t1, Evar_defined t2 -> eq_constr_univs_test d t1 t2 -| _ -> false - -let eq_evar_info d ei1 ei2 = - ei1 == ei2 || - eq_constr_univs_test d ei1.evar_concl ei2.evar_concl && - eq_named_context_val d (ei1.evar_hyps) (ei2.evar_hyps) && - eq_evar_body d ei1.evar_body ei2.evar_body - (** ppedrot: [eq_constr] may be a bit too permissive here *) - - (**********************************************************) (* Accessing metas *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 48704f75b..0765b951f 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -126,10 +126,6 @@ type evar_map (** Type of unification state. Essentially a bunch of state-passing data needed to handle incremental term construction. *) -val progress_evar_map : evar_map -> evar_map -> bool -(** Assuming that the second map extends the first one, this says if - some existing evar has been refined *) - val empty : evar_map (** The empty evar map. *) @@ -204,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map val undefined_map : evar_map -> evar_info Evar.Map.t (** Access the undefined evar mapping directly. *) -val eq_evar_info : evar_map -> evar_info -> evar_info -> bool -(** Compare the evar_info's up to the universe constraints of the evar map. *) - val drop_all_defined : evar_map -> evar_map (** {6 Instantiating partial terms} *) |