From 07686164a1279de0eff608f87ffe283dd34c1637 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 2 Apr 2002 07:58:21 +0000
Subject: - 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
---
 contrib/correctness/ptactic.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'contrib/correctness')

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
-- 
cgit v1.2.3