From 470cc2d01e6c4c2bc0ed109e20e1645c785dccf6 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:39:10 +0000
Subject: Normalise goals with respect to evars in the new tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17008 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/goal.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 2e7ee10bc0..5601cef823 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -355,6 +355,7 @@ let defs _ rdefs _ _ =
   !rdefs
 
 let enter f = (); fun env rdefs gl info ->
+  let info = Evarutil.nf_evar_info !rdefs info in
   f env !rdefs (Evd.evar_hyps info) (Evd.evar_concl info) gl
 
 (*** Conversion in goals ***)
-- 
cgit v1.2.3