From fb9442de3a7f5cab102f33a342a5fc7f63cd8f1c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 14 Feb 2020 13:01:12 +0100 Subject: Adding support for an "only parsing" modifier in "where"-based notations. Co-Authored-By: Théo Zimmermann --- test-suite/output/Inductive.out | 2 ++ test-suite/output/Inductive.v | 8 ++++++++ 2 files changed, 10 insertions(+) (limited to 'test-suite') diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 8ff571ae55..ff2556c5dc 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -5,3 +5,5 @@ Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x Arguments foo _%type_scope Arguments Foo _%type_scope +myprod unit bool + : Set diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v index 9eec9a7dad..db1276cb6c 100644 --- a/test-suite/output/Inductive.v +++ b/test-suite/output/Inductive.v @@ -5,3 +5,11 @@ Fail Inductive list' (A:Set) : Set := (* Check printing of let-ins *) #[universes(template)] Inductive foo (A : Type) (x : A) (y := x) := Foo. Print foo. + +(* Check where clause *) +Reserved Notation "x ** y" (at level 40, left associativity). +Inductive myprod A B := + mypair : A -> B -> A ** B + where "A ** B" := (myprod A B) (only parsing). + +Check unit ** bool. -- cgit v1.2.3