aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.md6
-rw-r--r--interp/constrexpr.ml6
-rw-r--r--parsing/notation_gram.ml7
-rw-r--r--parsing/notgram_ops.ml14
-rw-r--r--parsing/notgram_ops.mli1
-rw-r--r--parsing/parsing.mllib2
-rw-r--r--parsing/ppextend.ml21
-rw-r--r--parsing/ppextend.mli11
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/extraargs.mli2
-rw-r--r--plugins/ltac/pptactic.ml103
-rw-r--r--plugins/ltac/pptactic.mli29
-rw-r--r--plugins/ssr/ssrparser.mlg2
-rw-r--r--plugins/ssr/ssrparser.mli4
-rw-r--r--printing/genprint.ml8
-rw-r--r--printing/genprint.mli8
-rw-r--r--printing/ppconstr.ml85
-rw-r--r--printing/ppconstr.mli13
-rw-r--r--printing/printer.mli6
-rw-r--r--test-suite/success/Notations2.v13
-rw-r--r--vernac/metasyntax.ml122
21 files changed, 237 insertions, 228 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index cb6e695865..42dd2dd052 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -2,6 +2,12 @@
### ML API
+Types `precedence`, `parenRelation`, `tolerability` in
+`notgram_ops.ml` have been reworked. See `entry_level` and
+`entry_relative_level` in `constrexpr.ml`.
+
+### ML API
+
Exception handling:
- Coq's custom `Backtrace` module has been removed in favor of OCaml's
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 1d51109b7f..4bdacda529 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -20,8 +20,12 @@ type ident_decl = lident * universe_decl_expr option
type name_decl = lname * universe_decl_expr option
type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
+
+type entry_level = int
+type entry_relative_level = LevelLt of entry_level | LevelLe of entry_level | LevelSome
+
type notation_entry = InConstrEntry | InCustomEntry of string
-type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * int
+type notation_entry_level = InConstrEntrySomeLevel | InCustomEntryLevel of string * entry_level
type notation_key = string
(* A notation associated to a given parsing rule *)
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
index ffc92fa53a..427505c199 100644
--- a/parsing/notation_gram.ml
+++ b/parsing/notation_gram.ml
@@ -10,14 +10,11 @@
open Names
open Extend
+open Constrexpr
(** Dealing with precedences *)
-type precedence = int
-type parenRelation = L | E | Any | Prec of precedence
-type tolerability = precedence * parenRelation
-
-type level = Constrexpr.notation_entry * precedence * tolerability list * constr_entry_key list
+type level = notation_entry * entry_level * entry_relative_level list * constr_entry_key list
(* first argument is InCustomEntry s for custom entries *)
type grammar_constr_prod_item =
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index a84d2a4cb0..b6699493bb 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Notation
-open Notation_gram
+open Constrexpr
(* Register the level of notation for parsing and printing
(also register the parsing rule if not onlyprinting) *)
@@ -37,10 +37,11 @@ let get_defined_notations () =
open Extend
-let parenRelation_eq t1 t2 = match t1, t2 with
-| L, L | E, E | Any, Any -> true
-| Prec l1, Prec l2 -> Int.equal l1 l2
-| _ -> false
+let entry_relative_level_eq t1 t2 = match t1, t2 with
+| LevelLt n1, LevelLt n2 -> Int.equal n1 n2
+| LevelLe n1, LevelLe n2 -> Int.equal n1 n2
+| LevelSome, LevelSome -> true
+| (LevelLt _ | LevelLe _ | LevelSome), _ -> false
let production_position_eq pp1 pp2 = match (pp1,pp2) with
| BorderProd (side1,assoc1), BorderProd (side2,assoc2) -> side1 = side2 && assoc1 = assoc2
@@ -64,11 +65,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
- let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
let prod_eq (l1,pp1) (l2,pp2) =
not strict ||
(production_level_eq l1 l2 && production_position_eq pp1 pp2) in
- notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+ notation_entry_eq s1 s2 && Int.equal l1 l2 && List.equal entry_relative_level_eq t1 t2
&& List.equal (constr_entry_key_eq prod_eq) u1 u2
let level_eq = level_eq_gen false
diff --git a/parsing/notgram_ops.mli b/parsing/notgram_ops.mli
index 7c676fbb10..d8b7e8e4c1 100644
--- a/parsing/notgram_ops.mli
+++ b/parsing/notgram_ops.mli
@@ -13,6 +13,7 @@ open Constrexpr
open Notation_gram
val level_eq : level -> level -> bool
+val entry_relative_level_eq : entry_relative_level -> entry_relative_level -> bool
(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index 2154f2f881..12311f9cd9 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -2,8 +2,8 @@ Tok
CLexer
Extend
Notation_gram
-Ppextend
Notgram_ops
+Ppextend
Pcoq
G_constr
G_prim
diff --git a/parsing/ppextend.ml b/parsing/ppextend.ml
index 0277e79adb..393ab8a302 100644
--- a/parsing/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -12,7 +12,8 @@ open Util
open Pp
open CErrors
open Notation
-open Notation_gram
+open Constrexpr
+open Notgram_ops
(*s Pretty-print. *)
@@ -37,22 +38,22 @@ let ppcmd_of_cut = function
| PpBrk(n1,n2) -> brk(n1,n2)
type unparsing =
- | UnpMetaVar of int * parenRelation
- | UnpBinderMetaVar of int * parenRelation
- | UnpListMetaVar of int * parenRelation * unparsing list
- | UnpBinderListMetaVar of int * bool * unparsing list
+ | UnpMetaVar of entry_relative_level
+ | UnpBinderMetaVar of entry_relative_level
+ | UnpListMetaVar of entry_relative_level * unparsing list
+ | UnpBinderListMetaVar of bool * unparsing list
| UnpTerminal of string
| UnpBox of ppbox * unparsing Loc.located list
| UnpCut of ppcut
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * entry_level
type extra_unparsing_rules = (string * string) list
let rec unparsing_eq unp1 unp2 = match (unp1,unp2) with
- | UnpMetaVar (n1,p1), UnpMetaVar (n2,p2) -> n1 = n2 && p1 = p2
- | UnpBinderMetaVar (n1,p1), UnpBinderMetaVar (n2,p2) -> n1 = n2 && p1 = p2
- | UnpListMetaVar (n1,p1,l1), UnpListMetaVar (n2,p2,l2) -> n1 = n2 && p1 = p2 && List.for_all2eq unparsing_eq l1 l2
- | UnpBinderListMetaVar (n1,b1,l1), UnpBinderListMetaVar (n2,b2,l2) -> n1 = n2 && b1 = b2 && List.for_all2eq unparsing_eq l1 l2
+ | UnpMetaVar p1, UnpMetaVar p2 -> entry_relative_level_eq p1 p2
+ | UnpBinderMetaVar p1, UnpBinderMetaVar p2 -> entry_relative_level_eq p1 p2
+ | UnpListMetaVar (p1,l1), UnpListMetaVar (p2,l2) -> entry_relative_level_eq p1 p2 && List.for_all2eq unparsing_eq l1 l2
+ | UnpBinderListMetaVar (b1,l1), UnpBinderListMetaVar (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq l1 l2
| UnpTerminal s1, UnpTerminal s2 -> String.equal s1 s2
| UnpBox (b1,l1), UnpBox (b2,l2) -> b1 = b2 && List.for_all2eq unparsing_eq (List.map snd l1) (List.map snd l2)
| UnpCut p1, UnpCut p2 -> p1 = p2
diff --git a/parsing/ppextend.mli b/parsing/ppextend.mli
index 7996e7696d..346fc83f5f 100644
--- a/parsing/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Constrexpr
-open Notation_gram
(** {6 Pretty-print. } *)
@@ -31,15 +30,15 @@ val ppcmd_of_cut : ppcut -> Pp.t
(** Declare and look for the printing rule for symbolic notations *)
type unparsing =
- | UnpMetaVar of int * parenRelation
- | UnpBinderMetaVar of int * parenRelation
- | UnpListMetaVar of int * parenRelation * unparsing list
- | UnpBinderListMetaVar of int * bool * unparsing list
+ | UnpMetaVar of entry_relative_level
+ | UnpBinderMetaVar of entry_relative_level
+ | UnpListMetaVar of entry_relative_level * unparsing list
+ | UnpBinderListMetaVar of bool * unparsing list
| UnpTerminal of string
| UnpBox of ppbox * unparsing Loc.located list
| UnpCut of ppcut
-type unparsing_rule = unparsing list * precedence
+type unparsing_rule = unparsing list * entry_level
type extra_unparsing_rules = (string * string) list
val unparsing_eq : unparsing -> unparsing -> bool
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index bab6bfd78e..5835d75c79 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -298,7 +298,7 @@ END
let pr_by_arg_tac env sigma _prc _prlc prtac opt_c =
match opt_c with
| None -> mt ()
- | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t)
+ | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (Constrexpr.LevelLe 3) t)
}
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 6dd51e4e01..dd4195f2ef 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -67,7 +67,7 @@ val wit_by_arg_tac :
val pr_by_arg_tac :
Environ.env -> Evd.evar_map ->
- (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
val test_lpar_id_colon : unit Pcoq.Entry.t
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 7843faaef3..e2b8bcb5a9 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -17,7 +17,6 @@ open Constrexpr
open Genarg
open Geninterp
open Stdarg
-open Notation_gram
open Tactypes
open Locus
open Genredexpr
@@ -73,43 +72,43 @@ type 'a raw_extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
'a -> Pp.t
type 'a glob_extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
'a -> Pp.t
type 'a extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
'a -> Pp.t
type 'a raw_extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
+ entry_relative_level -> 'a -> Pp.t
type 'a glob_extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
+ entry_relative_level -> 'a -> Pp.t
type 'a extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+ entry_relative_level -> 'a -> Pp.t
let string_of_genarg_arg (ArgumentType arg) =
let rec aux : type a b c. (a, b, c) genarg_type -> string = function
@@ -294,7 +293,7 @@ let string_of_genarg_arg (ArgumentType arg) =
let pr _ = str "_" in
KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
- let pr_farg prtac arg = prtac (1, Any) (TacArg (CAst.make arg))
+ let pr_farg prtac arg = prtac LevelSome (TacArg (CAst.make arg))
let is_genarg tag wit =
let ArgT.Any tag = tag in
@@ -314,35 +313,35 @@ let string_of_genarg_arg (ArgumentType arg) =
let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t =
fun prtac symb arg -> match symb with
- | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
+ | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac LevelSome arg
| Extend.Ulist1 s | Extend.Ulist0 s ->
begin match get_list arg with
- | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
| Some l -> pr_sequence (pr_any_arg prtac s) l
end
| Extend.Ulist1sep (s, sep) | Extend.Ulist0sep (s, sep) ->
begin match get_list arg with
- | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
| Some l -> prlist_with_sep (fun () -> str sep) (pr_any_arg prtac s) l
end
| Extend.Uopt s ->
begin match get_opt arg with
- | None -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | None -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
| Some l -> pr_opt (pr_any_arg prtac s) l
end
| Extend.Uentry _ | Extend.Uentryl _ ->
- str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ str "ltac:(" ++ prtac LevelSome arg ++ str ")"
let pr_targ prtac symb arg = match symb with
| Extend.Uentry tag when is_genarg tag (ArgumentType wit_tactic) ->
- prtac (1, Any) arg
- | Extend.Uentryl (_, l) -> prtac (l, Any) arg
+ prtac LevelSome arg
+ | Extend.Uentryl (_, l) -> prtac LevelSome arg
| _ ->
match arg with
| TacGeneric arg ->
let pr l arg = prtac l (TacGeneric arg) in
pr_any_arg pr symb arg
- | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
+ | _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
let pr_raw_extend_rec prtac =
pr_extend_gen (pr_farg prtac)
@@ -630,7 +629,7 @@ let pr_goal_selector ~toplevel s =
let pr_then () = str ";"
- let ltop = (5,E)
+ let ltop = LevelLe 5
let lseq = 4
let ltactical = 3
let lorelse = 2
@@ -645,13 +644,13 @@ let pr_goal_selector ~toplevel s =
let ltatom = 1
let linfo = 5
- let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq
+ let level_of p = match p with LevelLe n -> n | LevelLt n -> n-1 | LevelSome -> lseq
(** A printer for tactics that polymorphically works on the three
"raw", "glob" and "typed" levels *)
type 'a printer = {
- pr_tactic : tolerability -> 'tacexpr -> Pp.t;
+ pr_tactic : entry_relative_level -> 'tacexpr -> Pp.t;
pr_constr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t;
pr_lconstr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t;
pr_dconstr : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t;
@@ -780,7 +779,7 @@ let pr_goal_selector ~toplevel s =
hov 1 (
primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++
- pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
+ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac
)
| TacAssert (ev,_,None,ipat,c) ->
hov 1 (
@@ -857,7 +856,7 @@ let pr_goal_selector ~toplevel s =
pr_with_bindings_arg_full (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) c)
l
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
- ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
+ ++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (LevelLe ltactical))) tac
)
| TacInversion (DepInversion (k,c,ids),hyp) ->
hov 1 (
@@ -893,11 +892,11 @@ let pr_goal_selector ~toplevel s =
let return (doc, l) = (tag tac doc, l) in
let (strm, prec) = return (match tac with
| TacAbstract (t,None) ->
- keyword "abstract " ++ pr_tac (labstract,L) t, labstract
+ keyword "abstract " ++ pr_tac (LevelLt labstract) t, labstract
| TacAbstract (t,Some s) ->
hov 0 (
keyword "abstract"
- ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc ()
+ ++ str" (" ++ pr_tac (LevelLt labstract) t ++ str")" ++ spc ()
++ keyword "using" ++ spc () ++ pr_id s),
labstract
| TacLetIn (recflag,llc,u) ->
@@ -906,7 +905,7 @@ let pr_goal_selector ~toplevel s =
(hv 0 (
pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc
++ spc () ++ keyword "in"
- ) ++ fnl () ++ pr_tac (llet,E) u),
+ ) ++ fnl () ++ pr_tac (LevelLe llet) u),
llet
| TacMatch (lz,t,lrul) ->
hov 0 (
@@ -931,17 +930,17 @@ let pr_goal_selector ~toplevel s =
hov 2 (
keyword "fun"
++ prlist pr_funvar lvar ++ str " =>" ++ spc ()
- ++ pr_tac (lfun,E) body),
+ ++ pr_tac (LevelLe lfun) body),
lfun
| TacThens (t,tl) ->
hov 1 (
- pr_tac (lseq,E) t ++ pr_then () ++ spc ()
+ pr_tac (LevelLe lseq) t ++ pr_then () ++ spc ()
++ pr_seq_body (pr_opt_tactic (pr_tac ltop)) tl),
lseq
| TacThen (t1,t2) ->
hov 1 (
- pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
- ++ pr_tac (lseq,L) t2),
+ pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc ()
+ ++ pr_tac (LevelLt lseq) t2),
lseq
| TacDispatch tl ->
pr_dispatch (pr_tac ltop) tl, lseq
@@ -949,78 +948,78 @@ let pr_goal_selector ~toplevel s =
pr_tac_extend (pr_tac ltop) tf t tr , lseq
| TacThens3parts (t1,tf,t2,tl) ->
hov 1 (
- pr_tac (lseq,E) t1 ++ pr_then () ++ spc ()
+ pr_tac (LevelLe lseq) t1 ++ pr_then () ++ spc ()
++ pr_then_gen (pr_tac ltop) tf t2 tl),
lseq
| TacTry t ->
hov 1 (
- keyword "try" ++ spc () ++ pr_tac (ltactical,E) t),
+ keyword "try" ++ spc () ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacDo (n,t) ->
hov 1 (
str "do" ++ spc ()
++ pr_or_var int n ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacTimeout (n,t) ->
hov 1 (
keyword "timeout "
++ pr_or_var int n ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacTime (s,t) ->
hov 1 (
keyword "time"
++ pr_opt qstring s ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacRepeat t ->
hov 1 (
keyword "repeat" ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacProgress t ->
hov 1 (
keyword "progress" ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacShowHyps t ->
hov 1 (
keyword "infoH" ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacInfo t ->
hov 1 (
keyword "info" ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
linfo
| TacOr (t1,t2) ->
hov 1 (
- pr_tac (lorelse,L) t1 ++ spc ()
+ pr_tac (LevelLt lorelse) t1 ++ spc ()
++ str "+" ++ brk (1,1)
- ++ pr_tac (lorelse,E) t2),
+ ++ pr_tac (LevelLe lorelse) t2),
lorelse
| TacOnce t ->
hov 1 (
keyword "once" ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacExactlyOnce t ->
hov 1 (
keyword "exactly_once" ++ spc ()
- ++ pr_tac (ltactical,E) t),
+ ++ pr_tac (LevelLe ltactical) t),
ltactical
| TacIfThenCatch (t,tt,te) ->
hov 1 (
- str"tryif" ++ spc() ++ pr_tac (ltactical,E) t ++ brk(1,1) ++
- str"then" ++ spc() ++ pr_tac (ltactical,E) tt ++ brk(1,1) ++
- str"else" ++ spc() ++ pr_tac (ltactical,E) te ++ brk(1,1)),
+ str"tryif" ++ spc() ++ pr_tac (LevelLe ltactical) t ++ brk(1,1) ++
+ str"then" ++ spc() ++ pr_tac (LevelLe ltactical) tt ++ brk(1,1) ++
+ str"else" ++ spc() ++ pr_tac (LevelLe ltactical) te ++ brk(1,1)),
ltactical
| TacOrelse (t1,t2) ->
hov 1 (
- pr_tac (lorelse,L) t1 ++ spc ()
+ pr_tac (LevelLt lorelse) t1 ++ spc ()
++ str "||" ++ brk (1,1)
- ++ pr_tac (lorelse,E) t2),
+ ++ pr_tac (LevelLe lorelse) t2),
lorelse
| TacFail (g,n,l) ->
let arg =
@@ -1042,7 +1041,7 @@ let pr_goal_selector ~toplevel s =
| TacSolve tl ->
keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
| TacComplete t ->
- pr_tac (lcomplete,E) t, lcomplete
+ pr_tac (LevelLe lcomplete) t, lcomplete
| TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
@@ -1398,10 +1397,10 @@ let () =
let () =
let printer env sigma _ _ prtac = prtac env sigma in
declare_extra_genarg_pprule_with_level wit_tactic printer printer printer
- ltop (0,E)
+ ltop (LevelLe 0)
let () =
let pr_unit _env _sigma _ _ _ _ () = str "()" in
let printer env sigma _ _ prtac = prtac env sigma in
declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit
- ltop (0,E)
+ ltop (LevelLe 0)
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 9cff3ea1eb..33db933168 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -16,7 +16,6 @@ open Geninterp
open Names
open Environ
open Constrexpr
-open Notation_gram
open Genintern
open Tacexpr
open Tactypes
@@ -29,43 +28,43 @@ type 'a raw_extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
'a -> Pp.t
type 'a glob_extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
'a -> Pp.t
type 'a extra_genarg_printer =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
'a -> Pp.t
type 'a raw_extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t) ->
+ entry_relative_level -> 'a -> Pp.t
type 'a glob_extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> glob_tactic_expr -> Pp.t) ->
+ entry_relative_level -> 'a -> Pp.t
type 'a extra_genarg_printer_with_level =
Environ.env -> Evd.evar_map ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
(Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
- (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ (Environ.env -> Evd.evar_map -> entry_relative_level -> Val.t -> Pp.t) ->
+ entry_relative_level -> 'a -> Pp.t
val declare_extra_genarg_pprule :
('a, 'b, 'c) genarg_type ->
@@ -78,7 +77,7 @@ val declare_extra_genarg_pprule_with_level :
'a raw_extra_genarg_printer_with_level ->
'b glob_extra_genarg_printer_with_level ->
'c extra_genarg_printer_with_level ->
- (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit
+ (* surroounded *) entry_relative_level -> (* non-surroounded *) entry_relative_level -> unit
val declare_extra_vernac_genarg_pprule :
('a, 'b, 'c) genarg_type ->
@@ -140,7 +139,7 @@ val pr_ltac_constant : ltac_constant -> Pp.t
val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t
-val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t
+val pr_raw_tactic_level : env -> Evd.evar_map -> entry_relative_level -> raw_tactic_expr -> Pp.t
val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t
@@ -155,10 +154,10 @@ val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t
val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) ->
('b, 'a) match_rule -> Pp.t
-val pr_value : tolerability -> Val.t -> Pp.t
+val pr_value : entry_relative_level -> Val.t -> Pp.t
-val ltop : tolerability
+val ltop : entry_relative_level
-val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> entry_relative_level -> 'a -> Pp.t) ->
'a Genprint.top_printer
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 21b832a326..3f67d55e73 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -90,7 +90,7 @@ let cast_arg wit v = Taccoerce.Value.cast (Genarg.topwit wit) v
* we thus save the lexer to restore it at the end of the file *)
let frozen_lexer = CLexer.get_keyword_state () ;;
-let tacltop = (5,Notation_gram.E)
+let tacltop = (LevelLe 5)
let pr_ssrtacarg env sigma _ _ prt = prt env sigma tacltop
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index e6b1706b41..53c895f9d9 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -15,12 +15,12 @@ open Ltac_plugin
val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
val pr_ssrtacarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
- (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c) -> 'c
+ (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c) -> 'c
val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t
val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
val pr_ssrtclarg : Environ.env -> Evd.evar_map -> 'a -> 'b ->
- (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
+ (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> 'c -> 'd) -> 'c -> 'd
val add_genarg : string -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) -> 'a Genarg.uniform_genarg_type
diff --git a/printing/genprint.ml b/printing/genprint.ml
index a04df31d30..a673cbd933 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -19,15 +19,15 @@ open Geninterp
(* Printing generic values *)
type 'a with_level =
- { default_already_surrounded : Notation_gram.tolerability;
- default_ensure_surrounded : Notation_gram.tolerability;
+ { default_already_surrounded : Constrexpr.entry_relative_level;
+ default_ensure_surrounded : Constrexpr.entry_relative_level;
printer : 'a }
type printer_result =
| PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t
type top_printer_result =
| TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index 21b8417ffa..59e36baeb6 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -13,15 +13,15 @@
open Genarg
type 'a with_level =
- { default_already_surrounded : Notation_gram.tolerability;
- default_ensure_surrounded : Notation_gram.tolerability;
+ { default_already_surrounded : Constrexpr.entry_relative_level;
+ default_ensure_surrounded : Constrexpr.entry_relative_level;
printer : 'a }
type printer_result =
| PrinterBasic of (Environ.env -> Evd.evar_map -> Pp.t)
-| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t) with_level
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Constrexpr.entry_relative_level -> Pp.t
type top_printer_result =
| TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2f60663c82..c2d760ae08 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -20,7 +20,6 @@ open Ppextend
open Glob_term
open Constrexpr
open Constrexpr_ops
-open Notation_gram
open Namegen
(*i*)
@@ -66,21 +65,16 @@ let tag_var = tag Tag.variable
let lapp = 10
let lposint = 0
let lnegint = 35 (* must be consistent with Notation "- x" *)
- let ltop = (200,E)
+ let ltop = LevelLe 200
let lproj = 1
let ldelim = 1
- let lsimpleconstr = (8,E)
- let lsimplepatt = (1,E)
-
- let prec_less child (parent,assoc) =
- if parent < 0 && Int.equal child lprod then true
- else
- let parent = abs parent in
- match assoc with
- | E -> (<=) child parent
- | L -> (<) child parent
- | Prec n -> child<=n
- | Any -> true
+ let lsimpleconstr = LevelLe 8
+ let lsimplepatt = LevelLe 1
+
+ let prec_less child = function
+ | LevelLt parent -> (<) child parent
+ | LevelLe parent -> if parent < 0 && Int.equal child lprod then true else child <= abs parent
+ | LevelSome -> true
let prec_of_prim_token = function
| Numeral (SPlus,_) -> lposint
@@ -98,22 +92,22 @@ let tag_var = tag Tag.variable
let rec aux = function
| [] ->
mt ()
- | UnpMetaVar (_, prec) as unp :: l ->
+ | UnpMetaVar prec as unp :: l ->
let c = pop env in
let pp2 = aux l in
- let pp1 = pr (n, prec) c in
+ let pp1 = pr prec c in
return unp pp1 pp2
- | UnpBinderMetaVar (_, prec) as unp :: l ->
+ | UnpBinderMetaVar prec as unp :: l ->
let c = pop bl in
let pp2 = aux l in
- let pp1 = pr_patt (n, prec) c in
+ let pp1 = pr_patt prec c in
return unp pp1 pp2
- | UnpListMetaVar (_, prec, sl) as unp :: l ->
+ | UnpListMetaVar (prec, sl) as unp :: l ->
let cl = pop envlist in
- let pp1 = prlist_with_sep (fun () -> aux sl) (pr (n,prec)) cl in
+ let pp1 = prlist_with_sep (fun () -> aux sl) (pr prec) cl in
let pp2 = aux l in
return unp pp1 pp2
- | UnpBinderListMetaVar (_, isopen, sl) as unp :: l ->
+ | UnpBinderListMetaVar (isopen, sl) as unp :: l ->
let cl = pop bll in
let pp2 = aux l in
let pp1 = pr_binders (fun () -> aux sl) isopen cl in
@@ -216,7 +210,7 @@ let tag_var = tag Tag.variable
let pr_expl_args pr (a,expl) =
match expl with
- | None -> pr (lapp,L) a
+ | None -> pr (LevelLt lapp) a
| Some {v=ExplByPos (n,_id)} ->
anomaly (Pp.str "Explicitation by position not implemented.")
| Some {v=ExplByName id} ->
@@ -243,31 +237,32 @@ let tag_var = tag Tag.variable
let las = lapp
let lpator = 0
let lpatrec = 0
+ let lpattop = LevelLe 200
let rec pr_patt sep inh p =
let (strm,prec) = match CAst.(p.v) with
| CPatRecord l ->
let pp (c, p) =
- pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p
+ pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p
in
(if l = [] then str "{| |}"
else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec
| CPatAlias (p, na) ->
- pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las
+ pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las
| CPatCstr (c, None, []) ->
pr_reference c, latom
| CPatCstr (c, None, args) ->
- pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp
| CPatCstr (c, Some args, []) ->
- str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) args, lapp
+ str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) args, lapp
| CPatCstr (c, Some expl_args, extra_args) ->
- surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (lapp,L)) expl_args)
- ++ prlist (pr_patt spc (lapp,L)) extra_args, lapp
+ surround (str "@" ++ pr_reference c ++ prlist (pr_patt spc (LevelLt lapp)) expl_args)
+ ++ prlist (pr_patt spc (LevelLt lapp)) extra_args, lapp
| CPatAtom (None) ->
str "_", latom
@@ -276,16 +271,16 @@ let tag_var = tag Tag.variable
pr_reference r, latom
| CPatOr pl ->
- let pp p = hov 0 (pr_patt mt (lpator,Any) p) in
+ let pp p = hov 0 (pr_patt mt lpattop p) in
surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator
| CPatNotation (_,(_,"( _ )"),([p],[]),[]) ->
- pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
+ pr_patt (fun()->str"(") lpattop p ++ str")", latom
| CPatNotation (which,s,(l,ll),args) ->
let strm_not, l_not = pr_notation (pr_patt mt) (fun _ _ -> mt ()) (fun _ _ _ -> mt()) which s (l,ll,[],[]) in
- (if List.is_empty args||prec_less l_not (lapp,L) then strm_not else surround strm_not)
- ++ prlist (pr_patt spc (lapp,L)) args, if not (List.is_empty args) then lapp else l_not
+ (if List.is_empty args||prec_less l_not (LevelLt lapp) then strm_not else surround strm_not)
+ ++ prlist (pr_patt spc (LevelLt lapp)) args, if not (List.is_empty args) then lapp else l_not
| CPatPrim p ->
pr_prim_token p, latom
@@ -440,7 +435,7 @@ let tag_var = tag Tag.variable
| Some t -> spc () ++ keyword "in" ++ spc () ++ pr_patt lsimplepatt t)
let pr_case_item pr (tm,as_clause, in_clause) =
- hov 0 (pr (lcast,E) tm ++ pr_asin pr as_clause in_clause)
+ hov 0 (pr (LevelLe lcast) tm ++ pr_asin pr as_clause in_clause)
let pr_case_type pr po =
match po with
@@ -456,17 +451,17 @@ let tag_var = tag Tag.variable
pr_case_type pr po
let pr_proj pr pr_app a f l =
- hov 0 (pr (lproj,E) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
+ hov 0 (pr (LevelLe lproj) a ++ cut() ++ str ".(" ++ pr_app pr f l ++ str ")")
let pr_appexpl pr (f,us) l =
hov 2 (
str "@" ++ pr_reference f ++
pr_universe_instance us ++
- prlist (pr_sep_com spc (pr (lapp,L))) l)
+ prlist (pr_sep_com spc (pr (LevelLt lapp))) l)
let pr_app pr a l =
hov 2 (
- pr (lapp,L) a ++
+ pr (LevelLt lapp) a ++
prlist (fun a -> spc () ++ pr_expl_args pr a) l)
let pr_record_body_gen pr l =
@@ -483,7 +478,7 @@ let tag_var = tag Tag.variable
let pr_dangling_with_for sep pr inherited a =
match a.v with
| (CFix (_,[_])|CCoFix(_,[_])) ->
- pr sep (latom,E) a
+ pr sep (LevelLe latom) a
| _ ->
pr sep inherited a
@@ -546,14 +541,14 @@ let tag_var = tag Tag.variable
let c,l1 = List.sep_last l1 in
let p = pr_proj (pr mt) pr_appexpl c (f,us) l1 in
if not (List.is_empty l2) then
- return (p ++ prlist (pr spc (lapp,L)) l2, lapp)
+ return (p ++ prlist (pr spc (LevelLt lapp)) l2, lapp)
else
return (p, lproj)
| CAppExpl ((None,qid,us),[t])
| CApp ((_, {v = CRef(qid,us)}),[t,None])
when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var ->
return (
- hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."),
+ hov 0 (str ".." ++ pr spc (LevelLe latom) t ++ spc () ++ str ".."),
larg
)
| CAppExpl ((None,f,us),l) ->
@@ -642,16 +637,16 @@ let tag_var = tag Tag.variable
return (pr_glob_sort s, latom)
| CCast (a,b) ->
return (
- hv 0 (pr mt (lcast,L) a ++ spc () ++
+ hv 0 (pr mt (LevelLt lcast) a ++ spc () ++
match b with
- | CastConv b -> str ":" ++ ws 1 ++ pr mt (-lcast,E) b
- | CastVM b -> str "<:" ++ ws 1 ++ pr mt (-lcast,E) b
- | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (-lcast,E) b
+ | CastConv b -> str ":" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
+ | CastVM b -> str "<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
+ | CastNative b -> str "<<:" ++ ws 1 ++ pr mt (LevelLe (-lcast)) b
| CastCoerce -> str ":>"),
lcast
)
| CNotation (_,(_,"( _ )"),([t],[],[],[])) ->
- return (pr (fun()->str"(") (max_int,L) t ++ str")", latom)
+ return (pr (fun()->str"(") ltop t ++ str")", latom)
| CNotation (which,s,env) ->
pr_notation (pr mt) pr_patt (pr_binders_gen (pr mt ltop)) which s env
| CGeneralization (bk,ak,c) ->
@@ -659,7 +654,7 @@ let tag_var = tag Tag.variable
| CPrim p ->
return (pr_prim_token p, prec_of_prim_token p)
| CDelimiters (sc,a) ->
- return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
+ return (pr_delimiters sc (pr mt (LevelLe ldelim) a), ldelim)
in
let loc = constr_loc a in
pr_with_comments ?loc
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index c17ca251a8..288fb251c4 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,9 +15,8 @@
open Libnames
open Constrexpr
open Names
-open Notation_gram
-val prec_less : precedence -> tolerability -> bool
+val prec_less : entry_level -> entry_relative_level -> bool
val pr_tight_coma : unit -> Pp.t
@@ -49,7 +48,7 @@ val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr
val pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t
val pr_lconstr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t
val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t
-val pr_constr_expr_n : Environ.env -> Evd.evar_map -> tolerability -> constr_expr -> Pp.t
+val pr_constr_expr_n : Environ.env -> Evd.evar_map -> entry_relative_level -> constr_expr -> Pp.t
type term_pr = {
pr_constr_expr : Environ.env -> Evd.evar_map -> constr_expr -> Pp.t;
@@ -76,8 +75,8 @@ val default_term_pr : term_pr
Which has the same type. We can turn a modular printer into a printer by
taking its fixpoint. *)
-val lsimpleconstr : tolerability
-val ltop : tolerability
+val lsimpleconstr : entry_relative_level
+val ltop : entry_relative_level
val modular_constr_pr :
- ((unit->Pp.t) -> tolerability -> constr_expr -> Pp.t) ->
- (unit->Pp.t) -> tolerability -> constr_expr -> Pp.t
+ ((unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t) ->
+ (unit->Pp.t) -> entry_relative_level -> constr_expr -> Pp.t
diff --git a/printing/printer.mli b/printing/printer.mli
index cd5151bd8f..24d0a8cf6a 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -51,7 +51,7 @@ val enable_goal_names_printing : bool ref
val pr_constr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t
val pr_lconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> constr -> Pp.t
-val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
+val pr_constr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> constr -> Pp.t
(** Same, but resilient to [Nametab] errors. Prints fully-qualified
names when [shortest_qualid_of_global] has failed. Prints "??"
@@ -63,7 +63,7 @@ val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t
val pr_econstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t
val pr_leconstr_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> EConstr.t -> Pp.t
-val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
+val pr_econstr_n_env : ?lax:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> EConstr.t -> Pp.t
val pr_etype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
val pr_letype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> EConstr.types -> Pp.t
@@ -100,7 +100,7 @@ val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp
val pr_ltype_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
val pr_type_env : ?lax:bool -> ?goal_concl_style:bool -> env -> evar_map -> types -> Pp.t
-val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
+val pr_closed_glob_n_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> Constrexpr.entry_relative_level -> closed_glob_constr -> Pp.t
val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name -> env -> evar_map -> closed_glob_constr -> Pp.t
val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index aa439fae12..b26e725d9b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -172,3 +172,16 @@ Notation "#" := 0 (only printing).
Print Visibility.
End Bug10750.
+
+Module M18.
+
+ Module A.
+ Module B.
+ Infix "+++" := Nat.add (at level 70).
+ End B.
+ End A.
+Import A.
+(* Check that the notation in module B is not visible *)
+Infix "+++" := Nat.add (at level 80).
+
+End M18.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index b0b8a7612e..afff0347f5 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -286,32 +286,30 @@ let pr_notation_entry = function
| InConstrEntry -> str "constr"
| InCustomEntry s -> str "custom " ++ str s
-let prec_assoc = let open Gramlib.Gramext in function
- | RightA -> (L,E)
- | LeftA -> (E,L)
- | NonA -> (L,L)
-
let precedence_of_position_and_level from_level = function
- | NumLevel n, BorderProd (_,None) -> n, Prec n
| NumLevel n, BorderProd (b,Some a) ->
- n, let (lp,rp) = prec_assoc a in if b == Left then lp else rp
- | NumLevel n, InternalProd -> n, Prec n
- | NextLevel, _ -> from_level, L
- | DefaultLevel, _ ->
- (* Fake value, waiting for PR#5 at herbelin's fork *) 200,
- Any
+ (let open Gramlib.Gramext in
+ match a, b with
+ | RightA, Left -> LevelLt n
+ | RightA, Right -> LevelLe n
+ | LeftA, Left -> LevelLe n
+ | LeftA, Right -> LevelLt n
+ | NonA, _ -> LevelLt n)
+ | NumLevel n, _ -> LevelLe n
+ | NextLevel, _ -> LevelLt from_level
+ | DefaultLevel, _ -> LevelSome
(** Computing precedences of subentries for parsing *)
let precedence_of_entry_type (from_custom,from_level) = function
| ETConstr (custom,_,x) when notation_entry_eq custom from_custom ->
precedence_of_position_and_level from_level x
- | ETConstr (custom,_,(NumLevel n,_)) -> n, Prec n
+ | ETConstr (custom,_,(NumLevel n,_)) -> LevelLe n
| ETConstr (custom,_,(NextLevel,_)) ->
user_err (strbrk "\"next level\" is only for sub-expressions in the same entry as where the notation is (" ++
quote (pr_notation_entry custom) ++ strbrk " is different from " ++
quote (pr_notation_entry from_custom) ++ str ").")
- | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in n, Prec n
- | _ -> 0, E (* should not matter *)
+ | ETPattern (_,n) -> let n = match n with None -> 0 | Some n -> n in LevelLe n
+ | _ -> LevelSome (* should not matter *)
(** Computing precedences for future insertion of parentheses at
the time of printing using hard-wired constr levels *)
@@ -320,14 +318,14 @@ let unparsing_precedence_of_entry_type from_level = function
(* Possible insertion of parentheses at printing time to deal
with precedence in a constr entry is managed using [prec_less]
in [ppconstr.ml] *)
- snd (precedence_of_position_and_level from_level x)
+ precedence_of_position_and_level from_level x
| ETConstr (custom,_,_) ->
(* Precedence of printing for a custom entry is managed using
explicit insertion of entry coercions at the time of building
a [constr_expr] *)
- Any
- | ETPattern (_,n) -> (* in constr *) Prec (match n with Some n -> n | None -> 0)
- | _ -> Any (* should not matter *)
+ LevelSome
+ | ETPattern (_,n) -> (* in constr *) LevelLe (match n with Some n -> n | None -> 0)
+ | _ -> LevelSome (* should not matter *)
(* Some breaking examples *)
(* "x = y" : "x /1 = y" (breaks before any symbol) *)
@@ -397,11 +395,11 @@ let unparsing_metavar i from typs =
let prec = unparsing_precedence_of_entry_type from x in
match x with
| ETConstr _ | ETGlobal | ETBigint ->
- UnpMetaVar (i,prec)
+ UnpMetaVar prec
| ETPattern _ ->
- UnpBinderMetaVar (i,prec)
+ UnpBinderMetaVar prec
| ETIdent ->
- UnpBinderMetaVar (i,prec)
+ UnpBinderMetaVar prec
| ETBinder isopen ->
assert false
@@ -455,10 +453,10 @@ let make_hunks etyps symbols from_level =
(* We add NonTerminal for simulation but remove it afterwards *)
else make true sl in
let hunk = match typ with
- | ETConstr _ -> UnpListMetaVar (i,prec,List.map snd sl')
+ | ETConstr _ -> UnpListMetaVar (prec,List.map snd sl')
| ETBinder isopen ->
check_open_binder isopen sl m;
- UnpBinderListMetaVar (i,isopen,List.map snd sl')
+ UnpBinderListMetaVar (isopen,List.map snd sl')
| _ -> assert false in
(None, hunk) :: make_with_space b prods
@@ -597,10 +595,10 @@ let hunks_of_format (from_level,(vars,typs)) symfmt =
if not (List.is_empty sl) then error_format ?loc:(find_prod_list_loc loc_slfmt fmt) ();
let symbs, l = aux (symbs,rfmt) in
let hunk = match typ with
- | ETConstr _ -> UnpListMetaVar (i,prec,slfmt)
+ | ETConstr _ -> UnpListMetaVar (prec,slfmt)
| ETBinder isopen ->
check_open_binder isopen sl m;
- UnpBinderListMetaVar (i,isopen,slfmt)
+ UnpBinderListMetaVar (isopen,slfmt)
| _ -> assert false in
symbs, hunk :: l
| symbs, (_,UnpBox (a,b)) :: fmt ->
@@ -745,15 +743,11 @@ let recompute_assoc typs = let open Gramlib.Gramext in
let pr_arg_level from (lev,typ) =
let pplev = function
- | (n,L) when Int.equal n from -> str "at next level"
- | (n,E) -> str "at level " ++ int n
- | (n,L) -> str "at level below " ++ int n
- | (n,Prec m) when Int.equal m n -> str "at level " ++ int n
- | (n,_) -> str "Unknown level" in
- Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++
- (match typ with
- | ETConstr _ | ETPattern _ -> spc () ++ pplev lev
- | _ -> mt ())
+ | LevelLt n when Int.equal n from -> spc () ++ str "at next level"
+ | LevelLe n -> spc () ++ str "at level " ++ int n
+ | LevelLt n -> spc () ++ str "at level below " ++ int n
+ | LevelSome -> mt () in
+ Ppvernac.pr_set_entry_type (fun _ -> (*TO CHECK*) mt()) typ ++ pplev lev
let pr_level ntn (from,fromlevel,args,typs) =
(match from with InConstrEntry -> mt () | InCustomEntry s -> str "in " ++ str s ++ spc()) ++
@@ -1417,34 +1411,36 @@ let load_notation =
load_notation_common true
let open_notation i (_, nobj) =
- let scope = nobj.notobj_scope in
- let (ntn, df) = nobj.notobj_notation in
- let pat = nobj.notobj_interp in
- let onlyprint = nobj.notobj_onlyprint in
- let deprecation = nobj.notobj_deprecation in
- let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
- let specific_ntn = (specific,ntn) in
- let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
- if Int.equal i 1 && fresh then begin
- (* Declare the interpretation *)
- let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
- (* Declare the uninterpretation *)
- if not nobj.notobj_onlyparse then
- Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
- (* Declare a possible coercion *)
- (match nobj.notobj_coercion with
- | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
- | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
- | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
- | None -> ())
- end;
- (* Declare specific format if any *)
- match nobj.notobj_specific_pp_rules with
- | Some pp_sy ->
- if specific_format_to_declare specific_ntn pp_sy then
- Ppextend.declare_specific_notation_printing_rules
- specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
- | None -> ()
+ if Int.equal i 1 then begin
+ let scope = nobj.notobj_scope in
+ let (ntn, df) = nobj.notobj_notation in
+ let pat = nobj.notobj_interp in
+ let onlyprint = nobj.notobj_onlyprint in
+ let deprecation = nobj.notobj_deprecation in
+ let specific = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in
+ let specific_ntn = (specific,ntn) in
+ let fresh = not (Notation.exists_notation_in_scope scope ntn onlyprint pat) in
+ if fresh then begin
+ (* Declare the interpretation *)
+ let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint deprecation in
+ (* Declare the uninterpretation *)
+ if not nobj.notobj_onlyparse then
+ Notation.declare_uninterpretation (NotationRule specific_ntn) pat;
+ (* Declare a possible coercion *)
+ (match nobj.notobj_coercion with
+ | Some (IsEntryCoercion entry) -> Notation.declare_entry_coercion specific_ntn entry
+ | Some (IsEntryGlobal (entry,n)) -> Notation.declare_custom_entry_has_global entry n
+ | Some (IsEntryIdent (entry,n)) -> Notation.declare_custom_entry_has_ident entry n
+ | None -> ())
+ end;
+ (* Declare specific format if any *)
+ match nobj.notobj_specific_pp_rules with
+ | Some pp_sy ->
+ if specific_format_to_declare specific_ntn pp_sy then
+ Ppextend.declare_specific_notation_printing_rules
+ specific_ntn ~extra:pp_sy.synext_extra pp_sy.synext_unparsing
+ | None -> ()
+ end
let cache_notation o =
load_notation_common false 1 o;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:54:19 +0000