From a3508843fa932cbc9a3c0b0d3dc5004752d2a8e4 Mon Sep 17 00:00:00 2001
From: gregoire
Date: Mon, 5 Dec 2005 10:16:24 +0000
Subject: changement d'egalite pour le named_context_val

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7640 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/refiner.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index fa29f5b4db..1bc19c9105 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -53,7 +53,7 @@ let norm_goal sigma gl =
     { evar_concl = ncl;
       evar_hyps = map_named_val red_fun gl.evar_hyps; 
       evar_body = gl.evar_body} in
-  if ngl = gl then None else Some ngl
+  if Evd.eq_evar_info ngl gl then None else Some ngl
 
 
 (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]]
@@ -81,7 +81,7 @@ let rec frontier p =
 	([p.goal],
 	 (fun lp' -> 
 	    let p' = List.hd lp' in
-            if p'.goal = p.goal then 
+            if Evd.eq_evar_info p'.goal p.goal then 
 	      p'
             else 
 	      errorlabstrm "Refiner.frontier"
@@ -101,7 +101,7 @@ let rec frontier_map_rec f n p =
   match p.ref with
     | None -> 
         let p' = f p in
-        if p'.goal == p.goal || p'.goal = p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then p'
         else 
 	  errorlabstrm "Refiner.frontier_map"
             (str"frontier_map was handed back a ill-formed proof.")
@@ -127,7 +127,7 @@ let rec frontier_mapi_rec f i p =
   match p.ref with
     | None -> 
         let p' = f i p in
-        if p'.goal == p.goal || p'.goal = p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then p'
         else 
 	  errorlabstrm "Refiner.frontier_mapi"
             (str"frontier_mapi was handed back a ill-formed proof.")
@@ -185,7 +185,7 @@ let lookup_tactic s =
 (* refiner r is a tactic applying the rule r *)
 
 let check_subproof_connection gl spfl =
-  list_for_all2eq (fun g pf -> g=pf.goal) gl spfl
+  list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
 
 let abstract_tactic_expr te tacfun gls =
   let (sgl_sigma,v) = tacfun gls in
@@ -459,7 +459,7 @@ let rec tclTHENLIST = function
 
 (* various progress criterions *)
 let same_goal gl subgoal = 
-  (hypotheses subgoal) = (hypotheses gl) &
+  eq_named_context_val (hypotheses subgoal) (hypotheses gl) &&
   eq_constr (conclusion subgoal) (conclusion gl)
 
 
-- 
cgit v1.2.3