aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/egramcoq.ml75
-rw-r--r--vernac/g_vernac.mlg6
-rw-r--r--vernac/metasyntax.ml8
-rw-r--r--vernac/obligations.ml40
-rw-r--r--vernac/ppvernac.ml2
-rw-r--r--vernac/record.ml4
-rw-r--r--vernac/vernacentries.ml17
-rw-r--r--vernac/vernacexpr.ml2
8 files changed, 71 insertions, 83 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 16101396cf..43abc0a200 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -33,24 +33,24 @@ open Pcoq
let constr_level = string_of_int
let default_levels =
- [200,Extend.RightA,false;
- 100,Extend.RightA,false;
- 99,Extend.RightA,true;
- 90,Extend.RightA,true;
- 10,Extend.LeftA,false;
- 9,Extend.RightA,false;
- 8,Extend.RightA,true;
- 1,Extend.LeftA,false;
- 0,Extend.RightA,false]
+ [200,Gramlib.Gramext.RightA,false;
+ 100,Gramlib.Gramext.RightA,false;
+ 99,Gramlib.Gramext.RightA,true;
+ 90,Gramlib.Gramext.RightA,true;
+ 10,Gramlib.Gramext.LeftA,false;
+ 9,Gramlib.Gramext.RightA,false;
+ 8,Gramlib.Gramext.RightA,true;
+ 1,Gramlib.Gramext.LeftA,false;
+ 0,Gramlib.Gramext.RightA,false]
let default_pattern_levels =
- [200,Extend.RightA,true;
- 100,Extend.RightA,false;
- 99,Extend.RightA,true;
- 90,Extend.RightA,true;
- 10,Extend.LeftA,false;
- 1,Extend.LeftA,false;
- 0,Extend.RightA,false]
+ [200,Gramlib.Gramext.RightA,true;
+ 100,Gramlib.Gramext.RightA,false;
+ 99,Gramlib.Gramext.RightA,true;
+ 90,Gramlib.Gramext.RightA,true;
+ 10,Gramlib.Gramext.LeftA,false;
+ 1,Gramlib.Gramext.LeftA,false;
+ 0,Gramlib.Gramext.RightA,false]
let default_constr_levels = (default_levels, default_pattern_levels)
@@ -70,28 +70,28 @@ let save_levels levels custom lev =
(* first LeftA, then RightA and NoneA together *)
let admissible_assoc = function
- | Extend.LeftA, Some (Extend.RightA | Extend.NonA) -> false
- | Extend.RightA, Some Extend.LeftA -> false
+ | Gramlib.Gramext.LeftA, Some (Gramlib.Gramext.RightA | Gramlib.Gramext.NonA) -> false
+ | Gramlib.Gramext.RightA, Some Gramlib.Gramext.LeftA -> false
| _ -> true
let create_assoc = function
- | None -> Extend.RightA
+ | None -> Gramlib.Gramext.RightA
| Some a -> a
let error_level_assoc p current expected =
let open Pp in
let pr_assoc = function
- | Extend.LeftA -> str "left"
- | Extend.RightA -> str "right"
- | Extend.NonA -> str "non" in
+ | Gramlib.Gramext.LeftA -> str "left"
+ | Gramlib.Gramext.RightA -> str "right"
+ | Gramlib.Gramext.NonA -> str "non" in
user_err
(str "Level " ++ int p ++ str " is already declared " ++
pr_assoc current ++ str " associative while it is now expected to be " ++
pr_assoc expected ++ str " associative.")
let create_pos = function
- | None -> Extend.First
- | Some lev -> Extend.After (constr_level lev)
+ | None -> Gramlib.Gramext.First
+ | Some lev -> Gramlib.Gramext.After (constr_level lev)
let find_position_gen current ensure assoc lev =
match lev with
@@ -121,13 +121,13 @@ let find_position_gen current ensure assoc lev =
updated, (Some (create_pos !after), Some assoc, Some (constr_level n), None)
| _ ->
(* The reinit flag has been updated *)
- updated, (Some (Extend.Level (constr_level n)), None, None, !init)
+ updated, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, !init)
end
with
(* Nothing has changed *)
Exit ->
(* Just inherit the existing associativity and name (None) *)
- current, (Some (Extend.Level (constr_level n)), None, None, None)
+ current, (Some (Gramlib.Gramext.Level (constr_level n)), None, None, None)
let rec list_mem_assoc_triple x = function
| [] -> false
@@ -186,15 +186,18 @@ let find_position accu custom forpat assoc level =
(* Binding constr entry keys to entries *)
(* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *)
-let camlp5_assoc = function
- | Some NonA | Some RightA -> RightA
- | None | Some LeftA -> LeftA
-
-let assoc_eq al ar = match al, ar with
-| NonA, NonA
-| RightA, RightA
-| LeftA, LeftA -> true
-| _, _ -> false
+let camlp5_assoc =
+ let open Gramlib.Gramext in function
+ | Some NonA | Some RightA -> RightA
+ | None | Some LeftA -> LeftA
+
+let assoc_eq al ar =
+ let open Gramlib.Gramext in
+ match al, ar with
+ | NonA, NonA
+ | RightA, RightA
+ | LeftA, LeftA -> true
+ | _, _ -> false
(* [adjust_level assoc from prod] where [assoc] and [from] are the name
and associativity of the level where to add the rule; the meaning of
@@ -204,7 +207,7 @@ let assoc_eq al ar = match al, ar with
Some None = NEXT
Some (Some (n,cur)) = constr LEVEL n
s.t. if [cur] is set then [n] is the same as the [from] level *)
-let adjust_level assoc from = function
+let adjust_level assoc from = let open Gramlib.Gramext in function
(* Associativity is None means force the level *)
| (NumLevel n,BorderProd (_,None)) -> Some (Some (n,true))
(* Compute production name on the right side *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index e3f6a87541..22528a607f 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1175,9 +1175,9 @@ GRAMMAR EXTEND Gram
| "in"; IDENT "custom"; x = IDENT -> { SetCustomEntry (x,None) }
| "in"; IDENT "custom"; x = IDENT; "at"; IDENT "level"; n = natural ->
{ SetCustomEntry (x,Some n) }
- | IDENT "left"; IDENT "associativity" -> { SetAssoc LeftA }
- | IDENT "right"; IDENT "associativity" -> { SetAssoc RightA }
- | IDENT "no"; IDENT "associativity" -> { SetAssoc NonA }
+ | IDENT "left"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.LeftA }
+ | IDENT "right"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.RightA }
+ | IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA }
| IDENT "only"; IDENT "printing" -> { SetOnlyPrinting }
| IDENT "only"; IDENT "parsing" -> { SetOnlyParsing }
| IDENT "compat"; s = STRING ->
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 5ab877fae2..82434afbbd 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -287,7 +287,7 @@ let pr_notation_entry = function
| InConstrEntry -> str "constr"
| InCustomEntry s -> str "custom " ++ str s
-let prec_assoc = function
+let prec_assoc = let open Gramlib.Gramext in function
| RightA -> (L,E)
| LeftA -> (E,L)
| NonA -> (L,L)
@@ -685,7 +685,7 @@ let border = function
| (_,(ETConstr(_,_,(_,BorderProd (_,a))))) :: _ -> a
| _ -> None
-let recompute_assoc typs =
+let recompute_assoc typs = let open Gramlib.Gramext in
match border typs, border (List.rev typs) with
| Some LeftA, Some RightA -> assert false
| Some LeftA, _ -> Some LeftA
@@ -802,7 +802,7 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
module NotationMods = struct
type notation_modifier = {
- assoc : gram_assoc option;
+ assoc : Gramlib.Gramext.g_assoc option;
level : int option;
custom : notation_entry;
etyps : (Id.t * simple_constr_prod_entry_key) list;
@@ -1230,7 +1230,7 @@ let compute_syntax_data local df modifiers =
let onlyprint = mods.only_printing in
let onlyparse = mods.only_parsing in
if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
- let assoc = Option.append mods.assoc (Some NonA) in
+ let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
let _ = check_useless_entry_types recvars mainvars mods.etyps in
let _ = check_binder_type recvars mods.etyps in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index cbb77057bd..4926b8c3e1 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -337,32 +337,20 @@ let assumption_message = Declare.assumption_message
let default_tactic = ref (Proofview.tclUNIT ())
(* true = hide obligations *)
-let hide_obligations = ref false
-
-let set_hide_obligations = (:=) hide_obligations
-let get_hide_obligations () = !hide_obligations
-
-open Goptions
-let () =
- declare_bool_option
- { optdepr = false;
- optname = "Hiding of Program obligations";
- optkey = ["Hide";"Obligations"];
- optread = get_hide_obligations;
- optwrite = set_hide_obligations; }
-
-let shrink_obligations = ref true
-
-let set_shrink_obligations = (:=) shrink_obligations
-let get_shrink_obligations () = !shrink_obligations
-
-let () =
- declare_bool_option
- { optdepr = true; (* remove in 8.8 *)
- optname = "Shrinking of Program obligations";
- optkey = ["Shrink";"Obligations"];
- optread = get_shrink_obligations;
- optwrite = set_shrink_obligations; }
+let get_hide_obligations =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~name:"Hidding of Program obligations"
+ ~key:["Hide";"Obligations"]
+ ~value:false
+
+
+let get_shrink_obligations =
+ Goptions.declare_bool_option_and_ref
+ ~depr:true (* remove in 8.8 *)
+ ~name:"Shrinking of Program obligations"
+ ~key:["Shrink";"Obligations"]
+ ~value:true
let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 2ddd210365..e7c1e29beb 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -380,7 +380,7 @@ open Pputils
let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
- let pr_syntax_modifier = function
+ let pr_syntax_modifier = let open Gramlib.Gramext in function
| SetItemLevel (l,bko,n) ->
prlist_with_sep sep_v2 str l ++ spc () ++ pr_at_level_opt n ++
pr_opt pr_constr_as_binder_kind bko
diff --git a/vernac/record.ml b/vernac/record.ml
index 81b33c2e11..f6dbcb5291 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -458,7 +458,7 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
-let declare_class finite def cum ubinders univs id idbuild paramimpls params arity
+let declare_class def cum ubinders univs id idbuild paramimpls params arity
template fieldimpls fields ?(kind=StructureComponent) coers priorities =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
@@ -671,7 +671,7 @@ let definition_structure udecl kind ~template cum poly finite records =
in
let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in
let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in
- declare_class finite def cum ubinders univs id.CAst.v idbuild
+ declare_class def cum ubinders univs id.CAst.v idbuild
implpars params arity template implfs fields coers priorities
| _ ->
let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fa1082473e..a157e01fc1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -582,10 +582,15 @@ let should_treat_as_cumulative cum poly =
else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
| None -> poly && Flags.is_polymorphic_inductive_cumulativity ()
-let uniform_inductive_parameters = ref false
+let get_uniform_inductive_parameters =
+ Goptions.declare_bool_option_and_ref
+ ~depr:false
+ ~name:"Uniform inductive parameters"
+ ~key:["Uniform"; "Inductive"; "Parameters"]
+ ~value:false
let should_treat_as_uniform () =
- if !uniform_inductive_parameters
+ if get_uniform_inductive_parameters ()
then ComInductive.UniformParameters
else ComInductive.NonUniformParameters
@@ -1538,14 +1543,6 @@ let () =
optwrite = Flags.make_polymorphic_inductive_cumulativity }
let () =
- declare_bool_option
- { optdepr = false;
- optname = "Uniform inductive parameters";
- optkey = ["Uniform"; "Inductive"; "Parameters"];
- optread = (fun () -> !uniform_inductive_parameters);
- optwrite = (fun b -> uniform_inductive_parameters := b) }
-
-let () =
declare_int_option
{ optdepr = false;
optname = "the level of inlining during functor application";
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 122005e011..1e6c40c829 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -167,7 +167,7 @@ type syntax_modifier =
| SetItemLevel of string list * Notation_term.constr_as_binder_kind option * Extend.production_level option
| SetLevel of int
| SetCustomEntry of string * int option
- | SetAssoc of Extend.gram_assoc
+ | SetAssoc of Gramlib.Gramext.g_assoc
| SetEntryType of string * Extend.simple_constr_prod_entry_key
| SetOnlyParsing
| SetOnlyPrinting
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 07:30:10 +0000