diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-27 22:08:57 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-27 22:08:57 +0000 |
| commit | 42ea537affb88f8e63499d909eb526e024fc0aec (patch) | |
| tree | 15d95ea521cd5b5ee592cee7c818cf45b413debf /tactics | |
| parent | fdad03c5c247ab6cfdde8fd58658d9e40a3fd8aa (diff) | |
Fix "Existing Instance" to handle globality information and "Existing
Class" too to handle references instead of just idents. Minor fix in
coqdoc. zeta-normalize setoid_rewrite proofs, removing useless
let-bindings generated by the tactic.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12609 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index ce6abc93e..50a735e58 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -825,6 +825,9 @@ let merge_evars (goal,cstr) = Evd.merge goal cstr let solve_constraints env evars = Typeclasses.resolve_typeclasses env ~split:false ~fail:true (merge_evars evars) +let nf_zeta = + Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = let concl, is_hyp = match clause with @@ -848,6 +851,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = let cstrevars = !evars in let evars = solve_constraints env cstrevars in let p = Evarutil.nf_isevar evars p in + let p = nf_zeta env evars p in let newt = Evarutil.nf_isevar evars newt in let abs = Option.map (fun (x, y) -> Evarutil.nf_isevar evars x, Evarutil.nf_isevar evars y) abs in |