diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-02 12:26:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-02 18:34:11 +0100 |
| commit | 9205d8dc7b9e97b6c2f0815fddc5673c21d11089 (patch) | |
| tree | cdb63debac7a78b66849ab8f747c5c7214bb1a7a /test-suite/bugs/closed/3347.v | |
| parent | 2374a23fb7ebfa547eb16ce2ab8dc9efb2a3f855 (diff) | |
Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.
Diffstat (limited to 'test-suite/bugs/closed/3347.v')
| -rw-r--r-- | test-suite/bugs/closed/3347.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v index 63d5c7a57..dcf5394ea 100644 --- a/test-suite/bugs/closed/3347.v +++ b/test-suite/bugs/closed/3347.v @@ -1,7 +1,7 @@ Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *) Set Universe Polymorphism. -Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). +Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing). Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. Inductive Unit : Type1 := tt : Unit. Fail Check Unit : Set. (* [Check Unit : Set] should fail if [Type1] is defined correctly *) |