From f9106194333c11ab86460660f3603565ecd7785a Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:41:06 +0000
Subject: Fix congruence: normalise hypotheses with respect to evars.

Detected in CompCert.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17026 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/cc/cctac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 32e6d914f9..a34cbf70fd 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -207,9 +207,9 @@ let make_prb gls depth additionnal_terms =
 		 neg_hyps:=(cid,nh):: !neg_hyps
 	     | `Rule patts -> add_quant state id true patts
 	     | `Nrule patts -> add_quant state id false patts
-	 end) (Environ.named_context_of_val (Goal.V82.hyps gls.sigma gls.it));
+	 end) (Environ.named_context_of_val (Goal.V82.nf_hyps gls.sigma gls.it));
     begin
-      match atom_of_constr env sigma (pf_concl gls) with
+      match atom_of_constr env sigma (Evarutil.nf_evar sigma (pf_concl gls)) with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
 	|	`Other g ->
 		  List.iter
-- 
cgit v1.2.3