aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/evarutil.ml10
-rw-r--r--pretyping/evd.ml13
-rw-r--r--pretyping/evd.mli3
-rw-r--r--printing/printer.ml2
-rw-r--r--proofs/evar_refiner.ml4
-rw-r--r--proofs/goal.ml6
-rw-r--r--tactics/evar_tactics.ml2
-rw-r--r--toplevel/himsg.ml4
9 files changed, 25 insertions, 21 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
diff --git a/printing/printer.ml b/printing/printer.ml
index 9b8c16938..90ddf8384 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -294,7 +294,7 @@ let pr_concl n sigma g =
(* display evar type: a context and a type *)
let pr_evgl_sign gl =
- let ps = pr_named_context_of (evar_unfiltered_env gl) in
+ let ps = pr_named_context_of (evar_env gl) in
let _, l = List.filter2 (fun b c -> not b) (evar_filter gl) (evar_context gl) in
let ids = List.rev (List.map pi1 l) in
let warn =
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 8f7513371..71a07326f 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -36,7 +36,7 @@ let define_and_solve_constraints evk c evd =
let w_refine (evk,evi) (ltac_var,rawc) sigma =
if Evd.is_defined sigma evk then
error "Instantiate called on already-defined evar";
- let env = Evd.evar_env evi in
+ let env = Evd.evar_filtered_env evi in
let sigma',typed_c =
try Pretyping.understand_ltac ~resolve_classes:true true
sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc
@@ -53,7 +53,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
(* Main component of vernac command Existential *)
let instantiate_pf_com evk com sigma =
let evi = Evd.find sigma evk in
- let env = Evd.evar_env evi in
+ let env = Evd.evar_filtered_env evi in
let rawc = Constrintern.intern_constr sigma env com in
let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in
sigma'
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a9aa4fa59..df3f6e0db 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -464,17 +464,17 @@ module V82 = struct
(* Old style env primitive *)
let env evars gl =
let evi = content evars gl in
- Evd.evar_env evi
+ Evd.evar_filtered_env evi
(* For printing *)
let unfiltered_env evars gl =
let evi = content evars gl in
- Evd.evar_unfiltered_env evi
+ Evd.evar_env evi
(* Old style hyps primitive *)
let hyps evars gl =
let evi = content evars gl in
- evi.Evd.evar_hyps
+ Evd.evar_hyps evi
(* Access to ".evar_concl" *)
let concl evars gl =
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index b7d5e1802..87aff97fb 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -41,7 +41,7 @@ let instantiate n (ist,rawc) ido gl =
if n <= 0 then error "Incorrect existential variable index.";
let evk,_ = List.nth evl (n-1) in
let evi = Evd.find sigma evk in
- let ltac_vars = Tacinterp.extract_ltac_constr_values ist (Evd.evar_env evi) in
+ let ltac_vars = Tacinterp.extract_ltac_constr_values ist (Evd.evar_filtered_env evi) in
let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
tclTHEN
(tclEVARS sigma')
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8289f6ca2..cfaea3d74 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -353,7 +353,7 @@ let explain_evar_kind env evi = function
| Evar_kinds.InternalHole ->
str "an internal placeholder" ++
Option.cata (fun evi ->
- let env = Evd.evar_env evi in
+ let env = Evd.evar_filtered_env evi in
str " of type " ++ pr_lconstr_env env evi.evar_concl ++
pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env)
(mt ()) evi
@@ -386,7 +386,7 @@ let explain_unsolvability = function
let explain_typeclass_resolution env evi k =
match Typeclasses.class_of_constr evi.evar_concl with
| Some c ->
- let env = Evd.evar_env evi in
+ let env = Evd.evar_filtered_env evi in
fnl () ++ str "Could not find an instance for " ++
pr_lconstr_env env evi.evar_concl ++
pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 21:07:50 +0000