diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2014-12-24 14:13:23 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2014-12-24 14:13:23 +0000 |
| commit | a9660f46b64132dec0d0efc8ff4419ec8899558b (patch) | |
| tree | f24eac9fb9a33cd4e81d71468d41ca1a4e9a4725 /coq/ex | |
| parent | 304aead5d68961c4a7e6085df27c921cfd52e714 (diff) | |
fixed a bug in command parsing for coq, due to recent changes.
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/indent.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v index 7218fa63..6644df83 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -15,22 +15,22 @@ Record a : Type := make_a { | C2 : forall n, test n | C3 : forall n, test n | C4 : forall n, test n. - + Inductive test2 : nat -> Prop := C1 : forall n, test n | C2 : forall n, test n | C3 : forall n, test n | C4 : forall n, test n. - + Let x : = 1. Let y := 2. - + Let y := (1, 2, 3, 4, 5). - Inductive test3 (* fixindent *) - : nat -> Prop - := C1 : forall n, test n - | C2 : forall n, test n + Inductive test3 (* fixindent *) + : nat -> Prop + := C1 : forall n, test n + | C2 : forall n, test n } Lemma toto:nat. |