Adding support for custom entries in notations.

- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
  entries. This typically corresponds to rules of the form
  'Notation "[ x ]" := x (x custom myconstr).' but also
  'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
  are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
  are natively recognized.

Incidentally merging ETConstr and ETConstrAsBinder.

Noticed in passing that parsing binder as custom was not done as in
constr.

Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.

3 files changed, 96 insertions, 11 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
new file mode 100644
index 0000000000..cef7d1a702
--- /dev/null
+++ b/test-suite/output/Notations4.out
@@ -0,0 +1,17 @@
+[< 0 > + < 1 > * < 2 >]
+     : nat
+[<< # 0 >>]
+     : option nat
+[1 {f 1}]
+     : Expr
+fun (x : nat) (y z : Expr) => [1 + y z + {f x}]
+     : nat -> Expr -> Expr -> Expr
+fun e : Expr =>
+match e with
+| [x y + z] => [x + y z]
+| [1 + 1] => [1]
+| _ => [e + e]
+end
+     : Expr -> Expr
+[(1 + 1)]
+     : Expr
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
new file mode 100644
index 0000000000..9738ce5a5e
--- /dev/null
+++ b/test-suite/output/Notations4.v
@@ -0,0 +1,68 @@
+(* An example with constr subentries *)
+
+Module A.
+
+Declare Custom Entry myconstr.
+
+Notation "[ x ]" := x (x custom myconstr at level 6).
+Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5).
+Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
+Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
+Check [ < 0 > + < 1 > * < 2 >].
+
+Declare Custom Entry anotherconstr.
+
+Notation "[ x ]" := x (x custom myconstr at level 6).
+Notation "<< x >>" := x (in custom myconstr at level 3, x custom anotherconstr at level 10).
+Notation "# x" := (Some x) (in custom anotherconstr at level 8, x constr at level 9).
+Check [ << # 0 >> ].
+
+End A.
+
+Module B.
+
+Inductive Expr :=
+ | Mul : Expr -> Expr -> Expr
+ | Add : Expr -> Expr -> Expr
+ | One : Expr.
+
+Declare Custom Entry expr.
+Notation "[ expr ]" := expr (expr custom expr at level 2).
+Notation "1" := One (in custom expr at level 0).
+Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity).
+Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
+Notation "( x )" := x (in custom expr at level 0, x at level 2).
+Notation "{ x }" := x (in custom expr at level 0, x constr).
+Notation "x" := x (in custom expr at level 0, x ident).
+
+Axiom f : nat -> Expr.
+Check [1 {f 1}].
+Check fun x y z => [1 + y z + {f x}].
+Check fun e => match e with
+| [x y + z] => [x + y z]
+| [1 + 1] => [1]
+| y => [y + e]
+end.
+
+End B.
+
+Module C.
+
+Inductive Expr :=
+ | Add : Expr -> Expr -> Expr
+ | One : Expr.
+
+Declare Custom Entry expr.
+Notation "[ expr ]" := expr (expr custom expr at level 1).
+Notation "1" := One (in custom expr at level 0).
+Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity).
+Notation "( x )" := x (in custom expr at level 0, x at level 2).
+
+(* Check the use of a two-steps coercion from constr to expr 1 then
+   from expr 0 to expr 2 (note that camlp5 parsing is more tolerant
+   and does not require parentheses to parse from level 2 while at
+   level 1) *)
+
+Check [1 + 1].
+
+End C.
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
index fa2393b910..32cfb354bf 100644
--- a/test-suite/output/ssr_explain_match.out
+++ b/test-suite/output/ssr_explain_match.out
@@ -1,35 +1,35 @@
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ - _ was already used in scope nat_scope.
+Warning: Notation "_ - _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ was already used in scope nat_scope.
+Warning: Notation "_ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ >= _ was already used in scope nat_scope.
+Warning: Notation "_ >= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ > _ was already used in scope nat_scope.
+Warning: Notation "_ > _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ <= _ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ <= _ was already used in scope nat_scope.
+Warning: Notation "_ < _ <= _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ <= _ < _ was already used in scope nat_scope.
+Warning: Notation "_ <= _ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ < _ < _ was already used in scope nat_scope.
+Warning: Notation "_ < _ < _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ + _ was already used in scope nat_scope.
+Warning: Notation "_ + _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 File "stdin", line 12, characters 0-61:
-Warning: Notation _ * _ was already used in scope nat_scope.
+Warning: Notation "_ * _" was already used in scope nat_scope.
 [notation-overridden,parsing]
 BEGIN INSTANCES
 instance: (x + y + z) matches: (x + y + z)