diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 24 | ||||
| -rw-r--r-- | proofs/clenv.mli | 2 |
2 files changed, 11 insertions, 15 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 465e7cc7a6..6fbe69647e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -52,24 +52,20 @@ let meta_ctr=ref 0;; let new_meta ()=incr meta_ctr;!meta_ctr;; -(* replaces a mapping of existentials into a mapping of metas. *) +(* replaces a mapping of existentials into a mapping of metas. + Problem if an evar appears in the type of another one (pops anomaly) *) let exist_to_meta sigma (emap, c) = - let subst = ref [] in - let mmap = ref [] in - 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 metamap = ref [] in + let change_exist evar = + let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in + let n = new_meta() in + metamap := (n, ty) :: !metamap; + mkMeta n in let rec replace c = match kind_of_term c with - Evar (k,_) -> - (try List.assoc k !subst - with Not_found -> c) + Evar (k,_ as ev) when not (Evd.in_dom sigma k) -> change_exist ev | _ -> map_constr replace c in - (!mmap, replace c) + (!metamap, replace c) type 'a freelisted = { rebus : 'a; diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 5968199359..2514b6e754 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -24,7 +24,7 @@ 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 : - Evd.evar_map -> (Evd.evar_map * constr) -> + Evd.evar_map -> Pretyping.open_constr -> ((int * types) list * constr) (* The Type of Constructions clausale environments. *) |