diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-04-16 12:30:42 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-04-16 12:30:42 +0000 |
| commit | a40c4b07059f754e63fa29787148cdab22359cb6 (patch) | |
| tree | e55100008e2a9615910648cede16436d21e36f7c /coq/example-x-symbols.v | |
| parent | 665fcf2a7667f428ca0be6fc31ba14117ab11c68 (diff) | |
little fix for x-symbols coq.
Diffstat (limited to 'coq/example-x-symbols.v')
| -rw-r--r-- | coq/example-x-symbols.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/example-x-symbols.v b/coq/example-x-symbols.v index c3bee71e..21d94b93 100644 --- a/coq/example-x-symbols.v +++ b/coq/example-x-symbols.v @@ -17,7 +17,7 @@ -foo_alpha_1_beta_3 (* this should appear like foo_a_1_B_3 where a and B are greek *) +foo'alpha'1_beta_3 (* this should appear like foo'a'1_B_3 where a and B are greek *) delta__1 delta^^1 (* greek delta with a sub 1 and the same with super 1 *) x_{a+b} x^{a+b} (* x with a+b subscripted and then superscripted *) philosophi (* no greek letter should appear on this line *) |