diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-18 12:05:15 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-18 12:05:15 +0000 |
| commit | 6f89e06a3230c3932cb43bd28e0f07f47d954a3f (patch) | |
| tree | 80e9985d920633e561f0039504e1d6bd5ab19fda /test-suite/output/Notations2.v | |
| parent | e15318e086e33f74664eed87322cd3ae20f5e13d (diff) | |
Fixed some printing bugs.
- Notations with coercions to funclass inserted were not working any
longer since r11886. Made a fix but maybe should we eventually type
the notations so that they have a canonical form (and in particular
with coercions pre-inserted?).
- Improved spacing management in printing extra tactic arguments "by" and "in".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12951 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Notations2.v')
| -rw-r--r-- | test-suite/output/Notations2.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 0d5cc9e24..3eeff401c 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -6,6 +6,15 @@ Inductive PAIR := P (n1:nat) (n2:nat). Coercion P : nat >-> Funclass. Check (2 3). +(* Check that notations with coercions to functions inserted still work *) +(* (were not working from revision 11886 to 12951) *) + +Record Binop := { binop :> nat -> nat -> nat }. +Class Plusop := { plusop : Binop; z : nat }. +Infix "[+]" := plusop (at level 40). +Instance Plus : Plusop := {| plusop := {| binop := plus |} ; z := 0 |}. +Check 2[+]3. + (* Test bug #2091 (variable le was printed using <= !) *) Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x. |