From 5da12797816cbde2cb70aab3795ca2eef795e059 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 8 Sep 2009 23:18:23 +0000 Subject: Remove some spaces --- coq/example-tokens.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'coq/example-tokens.v') 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 *) -- cgit v1.2.3