- modifs de la condition de garde pour mieux tenir compte des raisonnements

  par l'absurde
- un open_constr est maintenant un terme accompagne du sigma dans lequel il
  est typable (il manquait l'info concernant le contexte de typage des
  nouvelles evars)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2579 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 3 deletions

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index e78e9fd81c..c7f1fc2ed7 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -198,19 +198,23 @@ let (automatic : tactic) =
  * Vernac: Correctness <string> <program> [; <tactic>].
  *)
 
-let reduce_open_constr (em,c) =
+let reduce_open_constr (em0,c) =
   let existential_map_of_constr = 
     let rec collect em c = match kind_of_term c with
       | Cast (c',t) -> 
 	  (match kind_of_term c' with
-	     | Evar ev -> (ev,t) :: em
+	     | Evar (ev,_) ->
+                 if not (Evd.in_dom em ev) then
+                   Evd.add em ev (Evd.map em0 ev)
+                 else
+                   em
 	     | _ -> fold_constr collect em c)
       | Evar _ -> 
 	  assert false (* all existentials should be casted *)
       | _ -> 
 	  fold_constr collect em c
     in
-    collect []
+    collect Evd.empty
   in
   let c = Pred.red_cci c in
   let em = existential_map_of_constr c in