diff options
| author | aspiwack | 2013-11-02 15:34:26 +0000 |
|---|---|---|
| committer | aspiwack | 2013-11-02 15:34:26 +0000 |
| commit | 0a1202fae3a8ae8cf651c1b699545a8638ec579f (patch) | |
| tree | 652b6ae0fa3458d114467c31e1fe382bd1b755a3 /proofs | |
| parent | fe9258c4b228fb086baac7cd3d94207f2c43bb48 (diff) | |
A whole new implemenation of the refine tactic.
It now uses the same algorithm as pretyping does.
This produces pretty weird goal when refining pattern matching terms.
Modification of the pattern matching compilation algorithm are pending, hence I will let it be so for now.
The file Zsqrt_compat.v has two temporary [Admitted] related to this issue.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index da5cb6b19c..e590e7763b 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -198,7 +198,7 @@ module Refinable = struct post_defs in (* [delta_evars] in the shape of a list of [evar]-s*) - let delta_list = List.map fst (Evar.Map.bindings delta_evars) in + let delta_list = List.rev_map fst (Evar.Map.bindings delta_evars) in (* The variables in [myevars] are supposed to be stored in decreasing order. Breaking this invariant might cause many things to go wrong. *) @@ -233,10 +233,10 @@ module Refinable = struct open_constr let constr_of_open_constr handle check_type (evars, c) env rdefs gl info = - let delta = update_handle handle !rdefs evars in - rdefs := Evar.Map.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs; - if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info - else c + let _ = update_handle handle !rdefs evars in + rdefs := Evd.fold (fun ev evi evd -> if not (Evd.mem !rdefs ev) then Evd.add evd ev evi else evd) evars !rdefs; + if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info + else c end |