From bf578ad5e2f63b7a36aeaef5e0597101db1bd24a Mon Sep 17 00:00:00 2001
From: gregoire
Date: Fri, 2 Dec 2005 10:01:15 +0000
Subject: Changement des named_context Ajout de cast indiquant au kernel la
 strategie a suivre Resolution du bug sur les coinductifs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/cc/cctac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/cc')

diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml
index 71545d966e..a3e1902c06 100644
--- a/contrib/cc/cctac.ml
+++ b/contrib/cc/cctac.ml
@@ -131,7 +131,7 @@ let rec make_prb gls additionnal_terms =
 		      add_disequality state (HeqnH (idp,id)) ph nh) 
 		   !pos_hyps;
 		 neg_hyps:=(id,nh):: !neg_hyps
-	 end) gls.it.evar_hyps;
+	 end) (Environ.named_context_of_val gls.it.evar_hyps);
     begin
       match atom_of_constr env gls.it.evar_concl with
 	  `Eq (t,a,b) -> add_disequality state Goal a b
-- 
cgit v1.2.3