diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 18 | ||||
| -rw-r--r-- | proofs/clenv.mli | 4 |
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. *) |