diff options
| author | David Aspinall | 2010-08-25 11:36:14 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-08-25 11:36:14 +0000 |
| commit | c8f3f1f3374d295595673abc51e141d07f2cb204 (patch) | |
| tree | 9b8ca680968d3d9da4b797b2d741b49113f1e6e1 /coq/example-tokens.v | |
| parent | 2efdcfd66911748b8d6c2c9d4218eb131066cbff (diff) | |
Make tests succeed, although still two or three underlying bugs
Diffstat (limited to 'coq/example-tokens.v')
| -rw-r--r-- | coq/example-tokens.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/coq/example-tokens.v b/coq/example-tokens.v index fcd1a7d5..8308be6c 100644 --- a/coq/example-tokens.v +++ b/coq/example-tokens.v @@ -10,6 +10,8 @@ $Id$ *) +Module ExampleTokens. + Fixpoint toto (x:nat) {struct x} : nat := (* n a t should appear as |N *) match x with | O => O (* double arrow here *) @@ -72,9 +74,11 @@ Variable _alpha : Set. Variable alpha_ : Set. Lemma gamma__neqn : forall n__i:nat, n__i=n__i. - +Abort All. (* Tests of things that shouldn't be should be unicode characters: alpha lhd rhd lambda forall exists exists shouldn't be altered: exist foral *) + +End ExampleTokens.
\ No newline at end of file |