diff options
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 *) |