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

6 files changed, 21 insertions, 8 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 45ae911a2..0555096e2 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -106,6 +106,9 @@ let val_of_named_context ctxt =
 let lookup_named id env = Sign.lookup_named id env.env_named_context
 let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt
 
+let eq_named_context_val c1 c2 =
+   c1 == c2 || named_context_of_val c1 = named_context_of_val c2
+
 (* A local const is evaluable if it is defined  *)
 
 let named_type id env =
diff --git a/kernel/environ.mli b/kernel/environ.mli
index b8f565e45..1b1e227bb 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -37,6 +37,7 @@ type env
 val pre_env : env -> Pre_env.env
 
 type named_context_val
+val eq_named_context_val : named_context_val -> named_context_val -> bool
 
 val empty_env : env
 
@@ -45,6 +46,7 @@ val rel_context   : env -> rel_context
 val named_context : env -> named_context
 val named_context_val : env -> named_context_val
 
+
 val engagement    : env -> engagement option
 
 (* is the local context empty *)
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 8f0d2ebdd..c8be979e0 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -76,9 +76,9 @@ let crasy_val = (val_of_obj (repr 0))
 (* Functions *)
 type vfun  
 (* v = [Tc | c | fv1 | ... | fvn ] *)
-(*                  ^                       *)
+(*         ^                       *)
 (* [Tc | (Restart : c) | v | a1 | ... an] *)
-(*              ^                                  *)
+(*              ^                         *)
 
 (* Products *)
 type vprod 
@@ -220,6 +220,7 @@ type vswitch = {
     sw_env : vm_env
   } 
 
+(* Ne pas changer ce type sans modifier le code C *)
 type atom = 
   | Aid of id_key
   | Aiddef of id_key * values
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index c58d921eb..26df8f793 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -34,6 +34,12 @@ type evar_info = {
 
 let evar_context evi = named_context_of_val evi.evar_hyps
 
+let eq_evar_info ei1 ei2 =
+  ei1 == ei2 || 
+    eq_constr ei1.evar_concl ei2.evar_concl && 
+    eq_named_context_val (ei1.evar_hyps) (ei2.evar_hyps) &&
+    ei1.evar_body = ei2.evar_body
+
 module Evarmap = Intmap
 
 type evar_map1 = evar_info Evarmap.t
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 506ce4487..2f51ebf2d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -34,6 +34,7 @@ type evar_info = {
   evar_hyps : Environ.named_context_val;
   evar_body : evar_body}
 
+val eq_evar_info : evar_info -> evar_info -> bool
 val evar_context : evar_info -> named_context
 type evar_map
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index fa29f5b4d..1bc19c910 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)