diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-08 23:18:23 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-08 23:18:23 +0000 |
| commit | 5da12797816cbde2cb70aab3795ca2eef795e059 (patch) | |
| tree | c40eca1d212482d7078679208b80bce07c057dcc /coq/example-tokens.v | |
| parent | 153955899a42b9ef4c7ce5ad8cd9bcd82a39eb83 (diff) | |
Remove some spaces
Diffstat (limited to 'coq/example-tokens.v')
| -rw-r--r-- | coq/example-tokens.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/example-tokens.v b/coq/example-tokens.v index 0444162d..ba5939fc 100644 --- a/coq/example-tokens.v +++ b/coq/example-tokens.v @@ -10,7 +10,7 @@ Fixpoint toto (x:nat) {struct x} : nat := (* nat should appear as |N *) match x with | O => O (* double arrow here *) - | S => toto y (* double arrow here *) + | S y => toto y (* double arrow here *) end. Lemma titi : forall x:nat,x=x. (* symbolique for-all and nat *) |