diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2015-01-05 09:04:29 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2015-01-05 09:04:29 +0000 |
| commit | 453c56a955f15623a29ae41a4e767b7745e80076 (patch) | |
| tree | 6b633d479a3bcfe8e1263a4686c975aaac4476cc /coq/ex | |
| parent | 22d7dccdd23603d07975799a159623223cb31095 (diff) | |
trying to indent pending forall in the expected way
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/indent.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/coq/ex/indent.v b/coq/ex/indent.v index cd263810..c146f61d 100644 --- a/coq/ex/indent.v +++ b/coq/ex/indent.v @@ -43,7 +43,7 @@ Module foo. : nat -> Prop := C31 : forall n, test3 n | C32 : forall n, test3 n. - + End foo. Lemma toto:nat. |