From 42ea537affb88f8e63499d909eb526e024fc0aec Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sun, 27 Dec 2009 22:08:57 +0000
Subject: 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
---
 tactics/rewrite.ml4 | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index ce6abc93ec..50a735e58c 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
-- 
cgit v1.2.3