aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/comCoercion.ml19
-rw-r--r--vernac/comHints.ml2
-rw-r--r--vernac/metasyntax.ml3
-rw-r--r--vernac/prettyp.ml4
-rw-r--r--vernac/vernacentries.ml10
6 files changed, 25 insertions, 17 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 743d1d2026..5323c9f1c6 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -139,7 +139,7 @@ let build_beq_scheme_deps kn =
perfomed in a much cleaner way, e.g. using the kernel normal form of
constructor types and kernel whd_all for the argument types. *)
let rec aux accu c =
- let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+ let (c,a) = Reductionops.whd_betaiota_stack env Evd.empty EConstr.(of_constr c) in
let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
match Constr.kind c with
| Cast (x,_,_) -> aux accu (Term.applist (x,a))
@@ -238,7 +238,7 @@ let build_beq_scheme mode kn =
let compute_A_equality rel_list nlist eqA ndx t =
let lifti = ndx in
let rec aux c =
- let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+ let (c,a) = Reductionops.whd_betaiota_stack env Evd.empty EConstr.(of_constr c) in
let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
match Constr.kind c with
| Rel x -> mkRel (x-nlist+ndx)
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index d6be02245c..3cc5dd65af 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -111,7 +111,7 @@ la liste des variables dont depend la classe source
l'indice de la classe source dans la liste lp
*)
-let get_source lp source =
+let get_source env lp source =
let open Context.Rel.Declaration in
match source with
| None ->
@@ -120,7 +120,7 @@ let get_source lp source =
| [] -> raise Not_found
| LocalDef _ :: lt -> aux lt
| LocalAssum (_,t1) :: lt ->
- let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in
+ let cl1,u1,lv1 = find_class_type env Evd.empty (EConstr.of_constr t1) in
cl1,lt,lv1,1
in aux lp
| Some cl ->
@@ -130,17 +130,17 @@ let get_source lp source =
| LocalDef _ as decl :: lt -> aux (decl::acc) lt
| LocalAssum (_,t1) as decl :: lt ->
try
- let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in
+ let cl1,u1,lv1 = find_class_type env Evd.empty (EConstr.of_constr t1) in
if cl_typ_eq cl cl1 then cl1,acc,lv1,Context.Rel.nhyps lt+1
else raise Not_found
with Not_found -> aux (decl::acc) lt
in aux [] (List.rev lp)
-let get_target t ind =
+let get_target env t ind =
if (ind > 1) then
CL_FUN
else
- match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
+ match pi1 (find_class_type env Evd.empty (EConstr.of_constr t)) with
| CL_CONST p when Recordops.is_primitive_projection p ->
CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
| x -> x
@@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly =
match idf_opt with
| Some idf -> idf
| None ->
- let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in
+ let cl,u,_ = find_class_type env sigma (EConstr.of_constr t) in
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
@@ -298,14 +298,15 @@ let warn_uniform_inheritance =
let add_new_coercion_core coef stre poly source target isid =
check_source source;
- let t, _ = Typeops.type_of_global_in_context (Global.env ()) coef in
+ let env = Global.env () in
+ let t, _ = Typeops.type_of_global_in_context env coef in
if coercion_exists coef then raise (CoercionError AlreadyExists);
let lp,tg = decompose_prod_assum t in
let llp = List.length lp in
if Int.equal llp 0 then raise (CoercionError NotAFunction);
let (cls,ctx,lvs,ind) =
try
- get_source lp source
+ get_source env lp source
with Not_found ->
raise (CoercionError (NoSource source))
in
@@ -315,7 +316,7 @@ let add_new_coercion_core coef stre poly source target isid =
warn_uniform_inheritance coef;
let clt =
try
- get_target tg ind
+ get_target env tg ind
with Not_found ->
raise (CoercionError NoTarget)
in
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 2fd6fe2b29..ec37ec7fa8 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -33,7 +33,7 @@ let project_hint ~poly pri l2r r =
let p = if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
let sigma, p = Evd.fresh_global env sigma p in
let c =
- Reductionops.whd_beta sigma
+ Reductionops.whd_beta env sigma
(mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign))
in
let c =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 32affd562f..8435612abd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1757,7 +1757,8 @@ let cache_scope_command o =
let subst_scope_command (subst,(local,scope,o as x)) = match o with
| ScopeClasses cl ->
- let cl' = List.map_filter (subst_scope_class subst) cl in
+ let env = Global.env () in
+ let cl' = List.map_filter (subst_scope_class env subst) cl in
let cl' =
if List.for_all2eq (==) cl cl' then cl
else cl' in
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index a7170c8e18..faf53d3fad 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -906,7 +906,7 @@ let print_name env sigma na udecl =
match na with
| {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
print_any_name env sigma
- (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+ (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
ntn sc))
udecl
| {loc; v=Constrexpr.AN ref} ->
@@ -960,7 +960,7 @@ let print_about env sigma na udecl =
match na with
| {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
print_about_any ?loc env sigma
- (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
+ (Term (Notation.interp_notation_as_global_reference ?loc ~head:false (fun _ -> true)
ntn sc)) udecl
| {loc;v=Constrexpr.AN ref} ->
print_about_any ?loc env sigma (locate_any_name ref) udecl
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index aac0b54ed4..09201d727d 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -95,8 +95,14 @@ let show_proof ~pstate =
try
let pstate = Option.get pstate in
let p = Declare.Proof.get_proof pstate in
- let sigma, env = Declare.get_current_context pstate in
+ let sigma, _ = Declare.get_current_context pstate in
let pprf = Proof.partial_proof p in
+ (* In the absence of an environment explicitly attached to the
+ proof and on top of which side effects of the proof would be pushed, ,
+ we take the global environment which in practise should be a
+ superset of the initial environment in which the proof was
+ started *)
+ let env = Global.env() in
Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
(* We print nothing if there are no goals left *)
with
@@ -1779,7 +1785,7 @@ let interp_search_about_item env sigma =
try
let ref =
Notation.interp_notation_as_global_reference
- (fun _ -> true) s sc in
+ ~head:false (fun _ -> true) s sc in
GlobSearchSubPattern (Pattern.PRef ref)
with UserError _ ->
user_err ~hdr:"interp_search_about_item"
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 09:25:18 +0000