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/ppvernac.ml2
-rw-r--r--vernac/vernacexpr.ml2
5 files changed, 48 insertions, 45 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/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/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 14:22:02 +0000