diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2015-02-19 12:08:51 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-02-24 18:50:39 +0100 |
| commit | f7b29094fe7cc13ea475447bd30d9a8b942f0fef (patch) | |
| tree | b1533a863e91a2650e2706b4955337f526249b36 /pretyping/evd.ml | |
| parent | fc6d0fb650f57a764af6fe9be44677a69be11980 (diff) | |
[Proofview.tclPROGRESS]: do not consider that trivial goal instantiation is progress.
Also compare goals up to evar instantiation (otherwise no progress would be observed when only unification occurs, unless some [nf_evar] is done). Performance look unchanged so far.
Some code from [Evd] which was used only in [tclPROGRESS] have been moved out (and [progress_evar_map] was now dead, so I killed it).
Fixes bugs (one reported directly on coqdev, and #3412).
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 29 |
1 files changed, 0 insertions, 29 deletions
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 *) |