aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/auto_ind_decl.ml33
-rw-r--r--vernac/g_vernac.mlg11
-rw-r--r--vernac/library.ml7
-rw-r--r--vernac/vernacentries.ml25
-rw-r--r--vernac/vernacentries.mli2
-rw-r--r--vernac/vernacinterp.ml25
6 files changed, 42 insertions, 61 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 0c9b9c7255..f3ad324aa5 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -113,8 +113,8 @@ let mkFullInd (ind,u) n =
else mkIndU (ind,u)
let check_bool_is_defined () =
- try let _ = Typeops.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in ()
- with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
+ if not (Coqlib.has_ref "core.bool.type")
+ then raise (UndefinedCst "bool")
let check_no_indices mib =
if Array.exists (fun mip -> mip.mind_nrealargs <> 0) mib.mind_packets then
@@ -236,10 +236,11 @@ let build_beq_scheme mode kn =
(* Needs Hints, see test suite *)
let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in
let kneq = Constant.change_label kn eq_lbl in
- try let _ = Environ.constant_opt_value_in env (kneq, u) in
+ if Environ.mem_constant kneq env then
+ let _ = Environ.constant_opt_value_in env (kneq, u) in
Term.applist (mkConst kneq,a),
Evd.empty_side_effects
- with Not_found -> raise (ParameterWithoutEquality (GlobRef.ConstRef kn)))
+ else raise (ParameterWithoutEquality (GlobRef.ConstRef kn)))
| Proj _ -> raise (EqUnknown "projection")
| Construct _ -> raise (EqUnknown "constructor")
| Case _ -> raise (EqUnknown "match")
@@ -373,7 +374,7 @@ so from Ai we can find the correct eq_Ai bl_ai or lb_ai
let do_replace_lb mode lb_scheme_key aavoid narg p q =
let open EConstr in
let avoid = Array.of_list aavoid in
- let do_arg sigma hd v offset =
+ let do_arg env sigma hd v offset =
match kind sigma v with
| Var s ->
let x = narg*offset in
@@ -390,7 +391,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
Parameter (see example "J" in test file SchemeEquality.v) *)
let lbl = Label.to_string (Constant.label cst) in
let newlbl = if Int.equal offset 1 then ("eq_" ^ lbl) else (lbl ^ "_lb") in
- mkConst (Constant.change_label cst (Label.make newlbl))
+ let newcst = Constant.change_label cst (Label.make newlbl) in
+ if Environ.mem_constant newcst env then mkConst newcst
+ else raise (ConstructorWithNonParametricInductiveType (fst hd))
| _ -> raise (ConstructorWithNonParametricInductiveType (fst hd))
in
@@ -419,8 +422,8 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
Proofview.tclEVARMAP >>= fun sigma ->
let lb_args = Array.append (Array.append
v
- (Array.Smart.map (fun x -> do_arg sigma u x 1) v))
- (Array.Smart.map (fun x -> do_arg sigma u x 2) v)
+ (Array.Smart.map (fun x -> do_arg env sigma u x 1) v))
+ (Array.Smart.map (fun x -> do_arg env sigma u x 2) v)
in let app = if Array.is_empty lb_args
then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
in
@@ -433,7 +436,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let open EConstr in
let avoid = Array.of_list aavoid in
- let do_arg sigma hd v offset =
+ let do_arg env sigma hd v offset =
match kind sigma v with
| Var s ->
let x = narg*offset in
@@ -450,7 +453,9 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
Parameter (see example "J" in test file SchemeEquality.v) *)
let lbl = Label.to_string (Constant.label cst) in
let newlbl = if Int.equal offset 1 then ("eq_" ^ lbl) else (lbl ^ "_bl") in
- mkConst (Constant.change_label cst (Label.make newlbl))
+ let newcst = Constant.change_label cst (Label.make newlbl) in
+ if Environ.mem_constant newcst env then mkConst newcst
+ else raise (ConstructorWithNonParametricInductiveType (fst hd))
| _ -> raise (ConstructorWithNonParametricInductiveType (fst hd))
in
@@ -487,8 +492,8 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
in let bl_args =
Array.append (Array.append
v
- (Array.Smart.map (fun x -> do_arg sigma u x 1) v))
- (Array.Smart.map (fun x -> do_arg sigma u x 2) v )
+ (Array.Smart.map (fun x -> do_arg env sigma u x 1) v))
+ (Array.Smart.map (fun x -> do_arg env sigma u x 2) v )
in
let app = if Array.is_empty bl_args
then bl_t1 else mkApp (bl_t1,bl_args)
@@ -837,8 +842,8 @@ let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
(* Decidable equality *)
let check_not_is_defined () =
- try ignore (Coqlib.lib_ref "core.not.type")
- with Not_found -> raise (UndefinedCst "not")
+ if not (Coqlib.has_ref "core.not.type")
+ then raise (UndefinedCst "not")
(* {n=m}+{n<>m} part *)
let compute_dec_goal ind lnamesparrec nparrec =
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a1cdc718d7..1f52641b82 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -199,8 +199,8 @@ GRAMMAR EXTEND Gram
VernacAssumption (stre, nl, bl) }
| d = def_token; id = ident_decl; b = def_body ->
{ VernacDefinition (d, name_of_ident_decl id, b) }
- | IDENT "Let"; id = identref; b = def_body ->
- { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) }
+ | IDENT "Let"; id = ident_decl; b = def_body ->
+ { VernacDefinition ((DoDischarge, Let), name_of_ident_decl id, b) }
(* Gallina inductive declarations *)
| f = finite_token; indl = LIST1 inductive_definition SEP "with" ->
{ VernacInductive (f, indl) }
@@ -552,7 +552,6 @@ GRAMMAR EXTEND Gram
{ VernacDeclareModule (export, id, bl, mty) }
(* Section beginning *)
| IDENT "Section"; id = identref -> { VernacBeginSection id }
- | IDENT "Chapter"; id = identref -> { VernacBeginSection id }
(* This end a Section a Module or a Module Type *)
| IDENT "End"; id = identref -> { VernacEndSegment id }
@@ -695,17 +694,17 @@ GRAMMAR EXTEND Gram
| IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; qid = global; ud = OPT [ u = OPT univ_decl; d = def_body -> { (u,d) } ] ->
{ match ud with
| None ->
- VernacCanonical CAst.(make ~loc @@ AN qid)
+ VernacCanonical CAst.(make ?loc:qid.CAst.loc @@ AN qid)
| Some (u,d) ->
let s = coerce_reference_to_id qid in
- VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),u),d) }
+ VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d) }
| IDENT "Canonical"; OPT [ IDENT "Structure" -> {()} ]; ntn = by_notation ->
{ VernacCanonical CAst.(make ~loc @@ ByNotation ntn) }
(* Coercions *)
| IDENT "Coercion"; qid = global; u = OPT univ_decl; d = def_body ->
{ let s = coerce_reference_to_id qid in
- VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),u),d) }
+ VernacDefinition ((NoDischarge,Coercion),((CAst.make ?loc:qid.CAst.loc (Name s)),u),d) }
| IDENT "Identity"; IDENT "Coercion"; f = identref; ":";
s = class_rawexpr; ">->"; t = class_rawexpr ->
{ VernacIdentityCoercion (f, s, t) }
diff --git a/vernac/library.ml b/vernac/library.ml
index 7c629b08e7..1b0bd4c0f7 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -155,11 +155,12 @@ let register_loaded_library m =
let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
let f = prefix ^ "cmo" in
let f = Dynlink.adapt_filename f in
- if Coq_config.native_compiler then
- Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
+ Nativelib.link_library (Global.env()) ~prefix ~dirname ~basename:f
in
let rec aux = function
- | [] -> link (); [libname]
+ | [] ->
+ let () = if Flags.get_native_compiler () then link () in
+ [libname]
| m'::_ as l when DirPath.equal m' libname -> l
| m'::l' -> m' :: aux l' in
libraries_loaded_list := aux !libraries_loaded_list;
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2e509921c1..3195f339b6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1251,10 +1251,12 @@ let vernac_generalizable ~local =
let local = Option.default true local in
Implicit_quantifiers.declare_generalizable ~local
+let allow_sprop_opt_name = ["Allow";"StrictProp"]
+
let () =
declare_bool_option
{ optdepr = false;
- optkey = ["Allow";"StrictProp"];
+ optkey = allow_sprop_opt_name;
optread = (fun () -> Global.sprop_allowed());
optwrite = Global.set_allow_sprop }
@@ -1435,27 +1437,6 @@ let () =
optread = CWarnings.get_flags;
optwrite = CWarnings.set_flags }
-let () =
- declare_string_option
- { optdepr = false;
- optkey = ["NativeCompute"; "Profile"; "Filename"];
- optread = Nativenorm.get_profile_filename;
- optwrite = Nativenorm.set_profile_filename }
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["NativeCompute"; "Profiling"];
- optread = Nativenorm.get_profiling_enabled;
- optwrite = Nativenorm.set_profiling_enabled }
-
-let () =
- declare_bool_option
- { optdepr = false;
- optkey = ["NativeCompute"; "Timing"];
- optread = Nativenorm.get_timing_enabled;
- optwrite = Nativenorm.set_timing_enabled }
-
let _ =
declare_bool_option
{ optdepr = false;
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f5cf9702cd..2ac8458ad5 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -24,3 +24,5 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
(** Miscellaneous stuff *)
val command_focus : unit Proof.focus_kind
+
+val allow_sprop_opt_name : string list
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 15a19c06c2..eb299222dd 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -51,24 +51,17 @@ let interp_typed_vernac c ~stack =
(* Default proof mode, to be set at the beginning of proofs for
programs that cannot be statically classified. *)
-let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
-let get_default_proof_mode () = !default_proof_mode
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
-let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
-let set_default_proof_mode_opt name =
- default_proof_mode :=
- match Pvernac.lookup_proof_mode name with
+let get_default_proof_mode =
+ Goptions.declare_interpreted_string_option_and_ref
+ ~depr:false
+ ~key:proof_mode_opt_name
+ ~value:(Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
+ (fun name -> match Pvernac.lookup_proof_mode name with
| Some pm -> pm
- | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
-
-let proof_mode_opt_name = ["Default";"Proof";"Mode"]
-let () =
- Goptions.declare_string_option Goptions.{
- optdepr = false;
- optkey = proof_mode_opt_name;
- optread = get_default_proof_mode_opt;
- optwrite = set_default_proof_mode_opt;
- }
+ | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)))
+ Pvernac.proof_mode_to_string
(** A global default timeout, controlled by option "Set Default Timeout n".
Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 16:27:04 +0000