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/comInductive.ml2
-rw-r--r--vernac/library.ml4
-rw-r--r--vernac/metasyntax.ml26
-rw-r--r--vernac/prettyp.ml4
-rw-r--r--vernac/record.ml2
-rw-r--r--vernac/vernacentries.ml10
9 files changed, 44 insertions, 29 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/comInductive.ml b/vernac/comInductive.ml
index cc9b840bed..4242f06844 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -475,7 +475,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
let indnames = List.map (fun ind -> ind.ind_name) indl in
(* In case of template polymorphism, we need to compute more constraints *)
- let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in
+ let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
interp_params env0 udecl uparamsl paramsl
diff --git a/vernac/library.ml b/vernac/library.ml
index 85db501e84..c30331b221 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -89,6 +89,7 @@ type library_disk = {
type summary_disk = {
md_name : compilation_unit_name;
md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+ md_ocaml : string;
}
(*s Modules loaded in memory contain the following informations. They are
@@ -251,6 +252,7 @@ let intern_from_file f =
let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in
let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
ObjFile.close_in ch;
+ System.check_caml_version ~caml:lsd.md_ocaml ~file:f;
register_library_filename lsd.md_name f;
add_opaque_table lsd.md_name (ToFetch del_opaque);
let open Safe_typing in
@@ -401,6 +403,7 @@ let load_library_todo f =
let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in
let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in
ObjFile.close_in ch;
+ System.check_caml_version ~caml:s0.md_ocaml ~file:f;
if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
@@ -486,6 +489,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
let sd = {
md_name = dir;
md_deps = Array.of_list (current_deps ());
+ md_ocaml = Coq_config.caml_version;
} in
let md = {
md_compiled = cenv;
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3b9c771b93..8435612abd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1073,12 +1073,12 @@ let make_internalization_vars recvars mainvars typs =
let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
maintyps @ extratyps
-let make_interpretation_type isrec isonlybinding = function
+let make_interpretation_type isrec isonlybinding default_if_binding = function
(* Parsed as constr list *)
| ETConstr (_,None,_) when isrec -> NtnTypeConstrList
- (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
+ (* Parsed as constr, but interpreted as a binder *)
| ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
- | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
+ | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr default_if_binding)
(* Parsed as constr, interpreted as constr *)
| ETConstr (_,None,_) -> NtnTypeConstr
(* Others *)
@@ -1096,7 +1096,9 @@ let subentry_of_constr_prod_entry = function
| ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel
| _ -> InConstrEntrySomeLevel
-let make_interpretation_vars recvars allvars typs =
+let make_interpretation_vars
+ (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsIdent)
+ recvars allvars typs =
let eq_subscope (sc1, l1) (sc2, l2) =
Option.equal String.equal sc1 sc2 &&
List.equal String.equal l1 l2
@@ -1113,7 +1115,7 @@ let make_interpretation_vars recvars allvars typs =
Id.Map.mapi (fun x (isonlybinding, sc) ->
let typ = Id.List.assoc x typs in
((subentry_of_constr_prod_entry typ,sc),
- make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
+ make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding default_if_binding typ)) mainvars
let check_rule_productivity l =
if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
@@ -1755,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
@@ -1792,8 +1795,8 @@ let try_interp_name_alias = function
| _ -> raise Not_found
let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
- let vars,reversibility,pat =
- try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
+ let acvars,pat,reversibility =
+ try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible
with Not_found ->
let fold accu id = Id.Map.add id NtnInternTypeAny accu in
let i_vars = List.fold_left fold Id.Map.empty vars in
@@ -1801,10 +1804,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
ninterp_var_type = i_vars;
ninterp_rec_vars = Id.Map.empty;
} in
- let nvars, pat, reversibility = interp_notation_constr env nenv c in
- let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
- List.map map vars, reversibility, pat
+ interp_notation_constr env nenv c
in
+ let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,0))) in
+ let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] acvars (List.map in_pat vars) in
+ let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
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/record.ml b/vernac/record.ml
index 9fda98d08e..36254780cd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -121,7 +121,7 @@ let typecheck_params_and_fields def poly pl ps records =
any Set <= i constraint for universes that might actually be instantiated with Prop. *)
let is_template =
List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
- let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
+ let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
let () =
let error bk {CAst.loc; v=name} =
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-29 15:25:03 +0000