diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 28 | ||||
| -rw-r--r-- | proofs/clenvtac.ml | 2 |
2 files changed, 15 insertions, 15 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 37d54a4eea..2f0e472095 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -41,11 +41,11 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_nf_meta clenv c = nf_meta clenv.evd c -let clenv_term clenv c = meta_instance clenv.evd c -let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv -let clenv_value clenv = meta_instance clenv.evd clenv.templval -let clenv_type clenv = meta_instance clenv.evd clenv.templtyp +let clenv_nf_meta clenv c = nf_meta clenv.env clenv.evd c +let clenv_term clenv c = meta_instance clenv.env clenv.evd c +let clenv_meta_type clenv mv = Typing.meta_type clenv.env clenv.evd mv +let clenv_value clenv = meta_instance clenv.env clenv.evd clenv.templval +let clenv_type clenv = meta_instance clenv.env clenv.evd clenv.templtyp let refresh_undefined_univs clenv = match EConstr.kind clenv.evd clenv.templval.rebus with @@ -212,19 +212,19 @@ let clenv_assign mv rhs clenv = In any case, we respect the order given in A. *) -let clenv_metas_in_type_of_meta evd mv = - (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas +let clenv_metas_in_type_of_meta env evd mv = + (mk_freelisted (meta_instance env evd (meta_ftype evd mv))).freemetas let dependent_in_type_of_metas clenv mvs = List.fold_right - (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.evd mv)) + (fun mv -> Metaset.union (clenv_metas_in_type_of_meta clenv.env clenv.evd mv)) mvs Metaset.empty let dependent_closure clenv mvs = let rec aux mvs acc = Metaset.fold (fun mv deps -> - let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.evd mv in + let metas_of_meta_type = clenv_metas_in_type_of_meta clenv.env clenv.evd mv in aux metas_of_meta_type (Metaset.union deps metas_of_meta_type)) mvs acc in aux mvs mvs @@ -251,7 +251,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce (* Instantiate metas that create beta/iota redexes *) -let meta_reducible_instance evd b = +let meta_reducible_instance env evd b = let fm = b.freemetas in let fold mv accu = let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in @@ -261,7 +261,7 @@ let meta_reducible_instance evd b = in let metas = Metaset.fold fold fm Metamap.empty in let rec irec u = - let u = whd_betaiota Evd.empty u (* FIXME *) in + let u = whd_betaiota env Evd.empty u (* FIXME *) in match EConstr.kind evd u with | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) -> let m = destMeta evd (strip_outer_cast evd c) in @@ -314,12 +314,12 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv = { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd } let clenv_unique_resolver_gen ?(flags=default_unify_flags ()) clenv concl = - if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd clenv.templtyp.rebus))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd clenv.templtyp.rebus))) then clenv_unify CUMUL ~flags (clenv_type clenv) concl (clenv_unify_meta_types ~flags clenv) else clenv_unify CUMUL ~flags - (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv + (meta_reducible_instance clenv.env clenv.evd clenv.templtyp) concl clenv let old_clenv_unique_resolver ?flags clenv gl = let concl = Goal.V82.concl clenv.evd (sig_it gl) in @@ -535,7 +535,7 @@ let error_already_defined b = (str "Position " ++ int n ++ str" already defined.") let clenv_unify_binding_type clenv c t u = - if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.evd u))) then + if isMeta clenv.evd (fst (decompose_app_vect clenv.evd (whd_nored clenv.env clenv.evd u))) then (* Not enough information to know if some subtyping is needed *) CoerceToType, clenv, c else diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 695e103082..6f24310cdb 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -36,7 +36,7 @@ let clenv_cast_meta clenv = match EConstr.kind clenv.evd (strip_outer_cast clenv.evd u) with | Meta mv -> (try - let b = Typing.meta_type clenv.evd mv in + let b = Typing.meta_type clenv.env clenv.evd mv in assert (not (occur_meta clenv.evd b)); if occur_meta clenv.evd b then u else mkCast (mkMeta mv, DEFAULTcast, b) |