- 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

2 files changed, 13 insertions, 9 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 67de8df987..465e7cc7a6 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -53,17 +53,21 @@ let meta_ctr=ref 0;;
 let new_meta ()=incr meta_ctr;!meta_ctr;;
 
 (* replaces a mapping of existentials into a mapping of metas. *)
-let exist_to_meta (emap, c) =
+let exist_to_meta sigma (emap, c) =
   let subst = ref [] in
   let mmap = ref [] in
-  let add_binding (e,ty) =
-    let n = new_meta() in
-    subst := (e, mkMeta n) :: !subst;
-    mmap := (n, ty) :: !mmap in
-  List.iter add_binding emap;
+  let add_binding (e,ev_decl) =
+    if not (Evd.in_dom sigma e) then begin
+      let n = new_meta() in
+      subst := (e, mkMeta n) :: !subst;
+      mmap := (n, ev_decl.evar_concl) :: !mmap
+    end in
+  List.iter add_binding (Evd.to_list emap);
   let rec replace c =
     match kind_of_term c with
-        Evar k -> List.assoc k !subst
+        Evar (k,_) ->
+          (try List.assoc k !subst
+          with Not_found -> c)
       | _ -> map_constr replace c in
   (!mmap, replace c)
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 162698112c..5968199359 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -24,8 +24,8 @@ val new_meta : unit -> int
 (* [exist_to_meta] generates new metavariables for each existential
    and performs the replacement in the given constr *)
 val exist_to_meta :
-  ((existential * constr) list * constr) ->
-  ((int * constr) list * constr)
+  Evd.evar_map -> (Evd.evar_map * constr) ->
+  ((int * types) list * constr)
 
 (* The Type of Constructions clausale environments. *)