From 33d86118c7d1bfba31008b410d81c7f45dbdf092 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 29 Jul 2018 02:39:32 +0200
Subject: A test on the different ways to indicate the levels of a rule.
This is in preparation of changes in level_eq, to check that the
semantics is preserved.
---
test-suite/success/Notations2.v | 8 ++++++++
1 file changed, 8 insertions(+)
(limited to 'test-suite')
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 7c2cf3ee52..d01ebfb18e 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -126,3 +126,11 @@ Notation "'myexists' x , p" := (ex (fun x => p))
(at level 200, x ident, p at level 200, right associativity) : type_scope.
Check myexists I, I = 0. (* Should not be seen as a constructor *)
End M14.
+
+(* 15. Testing different ways to give the same levels without failing *)
+
+Module M15.
+ Local Notation "###### x" := (S x) (right associativity, at level 79, x at next level).
+ Fail Local Notation "###### x" := (S x) (right associativity, at level 79).
+ Local Notation "###### x" := (S x) (at level 79).
+End M15.
--
cgit v1.2.3
From 60daf674df3d11fa2948bbc7c9a928c09f22d099 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 25 Nov 2017 17:19:49 +0100
Subject: 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.
---
test-suite/coqdoc/links.html.out | 34 ++++++++---------
test-suite/coqdoc/links.tex.out | 34 ++++++++---------
test-suite/output/Notations4.out | 17 +++++++++
test-suite/output/Notations4.v | 68 +++++++++++++++++++++++++++++++++
test-suite/output/ssr_explain_match.out | 22 +++++------
5 files changed, 130 insertions(+), 45 deletions(-)
create mode 100644 test-suite/output/Notations4.out
create mode 100644 test-suite/output/Notations4.v
(limited to 'test-suite')
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out
index 5e4b676c2f..d2d4d5d764 100644
--- a/test-suite/coqdoc/links.html.out
+++ b/test-suite/coqdoc/links.html.out
@@ -60,32 +60,32 @@ Various checks for coqdoc
Definition f := ∀ C:Prop, C.
-Notation "n ++ m" := (plus n m).
+Notation "n ++ m" := (plus n m).
-Notation "n ++ m" := (mult n m).
+Notation "n ++ m" := (mult n m).
-Notation "n ** m" := (plus n m) (at level 60).
+Notation "n ** m" := (plus n m) (at level 60).
-Notation "n ▵ m" := (plus n m) (at level 60).
+Notation "n ▵ m" := (plus n m) (at level 60).
-Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).
+Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).
-Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A
+Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A
-where "x = y :> A" := (@eq A x y) : type_scope.
+where "x = y :> A" := (@eq A x y) : type_scope.
-Definition eq0 := 0 = 0 :> nat.
+Definition eq0 := 0 = 0 :> nat.
-Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).
+Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).
-Definition b_α := ((0#0;0) , (0 ** 0)).
+Definition b_α := ((0#0;0) , (0 ** 0)).
Notation h := a.
@@ -97,7 +97,7 @@ Various checks for coqdoc
Variables b' b2: nat.
- Notation "n + m" := (n ▵ m) : my_scope.
+ Notation "n + m" := (n ▵ m) : my_scope.
Delimit Scope my_scope with my.
@@ -106,19 +106,19 @@ Various checks for coqdoc
Notation l := 0.
- Definition α := (0 + l)%my.
+ Definition α := (0 + l)%my.
- Definition a' b := b'++0++b2 _ ++x b.
+ Definition a' b := b'++0++b2 _ ++x b.
- Definition c := {True}+{True}.
+ Definition c := {True}+{True}.
- Definition d := (1+2)%nat.
+ Definition d := (1+2)%nat.
- Lemma e : nat + nat.
+ Lemma e : nat + nat.
Admitted.
@@ -137,7 +137,7 @@ Various checks for coqdoc
Variables b2: nat.
- Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.
+ Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.
End test.
diff --git a/test-suite/coqdoc/links.tex.out b/test-suite/coqdoc/links.tex.out
index f42db99dc2..24f96ff1e6 100644
--- a/test-suite/coqdoc/links.tex.out
+++ b/test-suite/coqdoc/links.tex.out
@@ -51,34 +51,34 @@ Various checks for coqdoc
\coqdockw{Definition} \coqdef{Coqdoc.links.f}{f}{\coqdocdefinition{f}} := \coqdockw{\ensuremath{\forall}} \coqdocvar{C}:\coqdockw{Prop}, \coqdocvariable{C}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}).\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '++' x}{"}{"}n ++ m" := (\coqexternalref{mult}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{mult}} \coqdocvar{n} \coqdocvar{m}). \coqdocemptyline
\coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x '**' x}{"}{"}n ** m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x 'xE2x96xB5' x}{"}{"}n ▵ m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 60).\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::x ''' ''' '++' 'x' x}{"}{"}n '\_' ++ 'x' m" := (\coqexternalref{plus}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocabbreviation{plus}} \coqdocvar{n} \coqdocvar{m}) (\coqdoctac{at} \coqdockw{level} 3).\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{:type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol
+\coqdockw{Inductive} \coqdef{Coqdoc.links.eq}{eq}{\coqdocinductive{eq}} (\coqdocvar{A}:\coqdockw{Type}) (\coqdocvar{x}:\coqdocvariable{A}) : \coqdocvar{A} \coqexternalref{::type scope:x '->' x}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocnotation{\ensuremath{\rightarrow}}} \coqdockw{Prop} := \coqdef{Coqdoc.links.eq refl}{eq\_refl}{\coqdocconstructor{eq\_refl}} : \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} \coqdocvariable{x} \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}}\coqdocvariable{A}\coqdoceol
\coqdocnoindent
\coqdoceol
\coqdocnoindent
-\coqdockw{where} \coqdef{Coqdoc.links.:type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
+\coqdockw{where} \coqdef{Coqdoc.links.::type scope:x '=' x ':>' x}{"}{"}x = y :> A" := (@\coqref{Coqdoc.links.eq}{\coqdocinductive{eq}} \coqdocvar{A} \coqdocvar{x} \coqdocvar{y}) : \coqdocvar{type\_scope}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.:type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.eq0}{eq0}{\coqdocdefinition{eq0}} := 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{=}} 0 \coqref{Coqdoc.links.::type scope:x '=' x ':>' x}{\coqdocnotation{:>}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Notation} \coqdef{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{"}{"}( x \# y ; .. ; z )" := (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} .. (\coqexternalref{pair}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{pair}} \coqdocvar{x} \coqdocvar{y}) .. \coqdocvar{z}).\coqdoceol
\coqdocemptyline
\coqdocnoindent
-\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{:core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.b xCExB1}{b\_α}{\coqdocdefinition{b\_α}} := \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{(}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{\#}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{;}}0\coqref{Coqdoc.links.:::'(' x 'x23' x ';' '..' ';' x ')'}{\coqdocnotation{)}} \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{,}} \coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{(}}0 \coqref{Coqdoc.links.:::x '**' x}{\coqdocnotation{**}} 0\coqexternalref{::core scope:'(' x ',' x ',' '..' ',' x ')'}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{))}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Notation} \coqdef{Coqdoc.links.h}{h}{\coqdocabbreviation{h}} := \coqref{Coqdoc.links.a}{\coqdocdefinition{a}}.\coqdoceol
@@ -90,7 +90,7 @@ Various checks for coqdoc
\coqdockw{Variables} \coqdef{Coqdoc.links.test.b'}{b'}{\coqdocvariable{b'}} \coqdef{Coqdoc.links.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
-\coqdockw{Notation} \coqdef{Coqdoc.links.test.:my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol
+\coqdockw{Notation} \coqdef{Coqdoc.links.test.::my scope:x '+' x}{"}{"}n + m" := (\coqdocvar{n} \coqref{Coqdoc.links.:::x 'xE2x96xB5' x}{\coqdocnotation{▵}} \coqdocvar{m}) : \coqdocvar{my\_scope}.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
\coqdockw{Delimit} \coqdockw{Scope} \coqdocvar{my\_scope} \coqdockw{with} \coqdocvar{my}.\coqdoceol
@@ -99,19 +99,19 @@ Various checks for coqdoc
\coqdockw{Notation} \coqdef{Coqdoc.links.l}{l}{\coqdocabbreviation{l}} := 0.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.:my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.xCExB1}{α}{\coqdocdefinition{α}} := (0 \coqref{Coqdoc.links.test.::my scope:x '+' x}{\coqdocnotation{+}} \coqref{Coqdoc.links.l}{\coqdocabbreviation{l}})\%\coqdocvar{my}.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.a'}{a'}{\coqdocdefinition{a'}} \coqdocvar{b} := \coqdocvariable{b'}\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}0\coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}}\coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}}\coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b}.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{:type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.c}{c}{\coqdocdefinition{c}} := \coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}+\{}}\coqexternalref{True}{http://coq.inria.fr/stdlib/Coq.Init.Logic}{\coqdocinductive{True}}\coqexternalref{::type scope:'x7B' x 'x7D' '+' 'x7B' x 'x7D'}{http://coq.inria.fr/stdlib/Coq.Init.Specif}{\coqdocnotation{\}}}.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.d}{d}{\coqdocdefinition{d}} := (1\coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}}2)\%\coqdocvar{nat}.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
-\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{:type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
+\coqdockw{Lemma} \coqdef{Coqdoc.links.e}{e}{\coqdoclemma{e}} : \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}} \coqexternalref{::type scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocnotation{+}} \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
\coqdocindent{2.00em}
\coqdocvar{Admitted}.\coqdoceol
\coqdocemptyline
@@ -131,7 +131,7 @@ Various checks for coqdoc
\coqdockw{Variables} \coqdef{Coqdoc.links.test2.test.b2}{b2}{\coqdocvariable{b2}}: \coqexternalref{nat}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocinductive{nat}}.\coqdoceol
\coqdocemptyline
\coqdocindent{3.00em}
-\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{:nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol
+\coqdockw{Definition} \coqdef{Coqdoc.links.a''}{a'{}'}{\coqdocdefinition{a'{}'}} \coqdocvar{b} := \coqdocvariable{b'} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqexternalref{O}{http://coq.inria.fr/stdlib/Coq.Init.Datatypes}{\coqdocconstructor{O}} \coqref{Coqdoc.links.:::x '++' x}{\coqdocnotation{++}} \coqdocvariable{b2} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{\_}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{++}} \coqref{Coqdoc.links.:::x ''' ''' '++' 'x' x}{\coqdocnotation{x}} \coqdocvariable{b} \coqexternalref{::nat scope:x '+' x}{http://coq.inria.fr/stdlib/Coq.Init.Peano}{\coqdocnotation{+}} \coqref{Coqdoc.links.h}{\coqdocabbreviation{h}} 0.\coqdoceol
\coqdocemptyline
\coqdocindent{2.00em}
\coqdockw{End} \coqref{Coqdoc.links.test2.test}{\coqdocsection{test}}.\coqdoceol
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)
--
cgit v1.2.3
From a90aa1a2d7f0fd12621e744a67cc8c2abd24f9f8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 29 Jun 2018 12:13:00 +0200
Subject: Supporting locality flag for custom entries + compatibility with
modules.
Also prevents to use an entry name already defined.
---
test-suite/success/Notations2.v | 20 ++++++++++++++++++++
1 file changed, 20 insertions(+)
(limited to 'test-suite')
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index d01ebfb18e..1b33863e3b 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -134,3 +134,23 @@ Module M15.
Fail Local Notation "###### x" := (S x) (right associativity, at level 79).
Local Notation "###### x" := (S x) (at level 79).
End M15.
+
+(* 16. Some test about custom entries *)
+Module M16.
+ (* Test locality *)
+ Local Declare Custom Entry foo.
+ Fail Notation "#" := 0 (in custom foo). (* Should be local *)
+ Local Notation "#" := 0 (in custom foo).
+
+ (* Test import *)
+ Module A.
+ Declare Custom Entry foo2.
+ End A.
+ Fail Notation "##" := 0 (in custom foo2).
+ Import A.
+ Local Notation "##" := 0 (in custom foo2).
+
+ (* Test Print Grammar *)
+ Print Grammar foo.
+ Print Grammar foo2.
+End M16.
--
cgit v1.2.3