diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 10 | ||||
| -rw-r--r-- | pretyping/evd.ml | 13 | ||||
| -rw-r--r-- | pretyping/evd.mli | 3 |
4 files changed, 16 insertions, 12 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 52ef44672..ca5ed190f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -636,7 +636,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = try let args = Array.to_list args in let evi = Evd.find_undefined evd evk in - let env_evar = evar_env evi in + let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in let filter = evar_filter evi in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f4f373754..fcc284832 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1452,7 +1452,7 @@ type conv_fun = let check_evar_instance evd evk1 body conv_algo = let evi = Evd.find evd evk1 in - let evenv = evar_unfiltered_env evi in + let evenv = evar_env evi in (* FIXME: The body might be ill-typed when this is called from w_merge *) let ty = try Retyping.get_type_of evenv evd body @@ -1571,7 +1571,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs = raise (NotEnoughInformationToProgress sols); (* No unique projection but still restrict to where it is possible *) (* materializing is necessary, but is restricting useful? *) - let ty = find_solution_type (evar_env evi) sols in + let ty = find_solution_type (evar_filtered_env evi) sols in let sign = evar_filtered_context evi in let ty' = instantiate_evar sign ty (Array.to_list argsv) in let (evd,evar,(evk',argsv' as ev')) = @@ -1711,7 +1711,7 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs = * Another problem is that type variables are evars of type Type let _ = try - let env = evar_env evi in + let env = evar_filtered_env evi in let ty = evi.evar_concl in Typing.check env evd' body ty with e -> @@ -1963,7 +1963,7 @@ let idx = Id.of_string "x" let define_pure_evar_as_product evd evk = let evi = Evd.find_undefined evd evk in - let evenv = evar_unfiltered_env evi in + let evenv = evar_env evi in let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in let evd1,dom = new_type_evar evd evenv ~filter:(evar_filter evi) in let evd2,rng = @@ -1997,7 +1997,7 @@ let define_evar_as_product evd (evk,args) = let define_pure_evar_as_lambda env evd evk = let evi = Evd.find_undefined evd evk in - let evenv = evar_unfiltered_env evi in + let evenv = evar_env evi in let typ = whd_betadeltaiota env evd (evar_concl evi) in let evd1,(na,dom,rng) = match kind_of_term typ with | Prod (na,dom,rng) -> (evd,(na,dom,rng)) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index a6049d0cf..4208a3763 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -50,14 +50,17 @@ let make_evar hyps ccl = { } let evar_concl evi = evi.evar_concl -let evar_hyps evi = evi.evar_hyps -let evar_context evi = named_context_of_val evi.evar_hyps -let evar_body evi = evi.evar_body let evar_filter evi = evi.evar_filter -let evar_unfiltered_env evi = Global.env_of_context evi.evar_hyps +let evar_body evi = evi.evar_body +let evar_context evi = named_context_of_val evi.evar_hyps let evar_filtered_context evi = snd (List.filter2 (fun b c -> b) (evar_filter evi) (evar_context evi)) -let evar_env evi = +let evar_hyps evi = evi.evar_hyps +let evar_filtered_hyps evi = + List.fold_right push_named_context_val (evar_filtered_context evi) + empty_named_context_val +let evar_env evi = Global.env_of_context evi.evar_hyps +let evar_filtered_env evi = List.fold_right push_named (evar_filtered_context evi) (reset_context (Global.env())) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 86ec47d3e..53956f99b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -111,10 +111,11 @@ val evar_concl : evar_info -> constr val evar_context : evar_info -> named_context val evar_filtered_context : evar_info -> named_context val evar_hyps : evar_info -> named_context_val +val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body val evar_filter : evar_info -> bool list -val evar_unfiltered_env : evar_info -> env val evar_env : evar_info -> env +val evar_filtered_env : evar_info -> env (*** Unification state ***) type evar_map |