From 803614383b7247bd7dd7739cc24749de245ae7c9 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 30 Aug 2004 13:36:53 +0000 Subject: debugged the indentation of coq (bug report of Batsiaan Zapf august 3rd 2004). I found another bug (infinite loop due to an error in coq-back-to-indentation-prevline). --- coq/ex-module.v | 35 +++++++++++++++++------------------ 1 file changed, 17 insertions(+), 18 deletions(-) (limited to 'coq/ex-module.v') diff --git a/coq/ex-module.v b/coq/ex-module.v index 240d0ad1..5b9d638a 100644 --- a/coq/ex-module.v +++ b/coq/ex-module.v @@ -72,26 +72,25 @@ Module Type N'. End N''. Declare Module N':M.SIG. (* no interactive def started *) - Declare Module N''':= N'. (* no interactive def started *) - Declare Module N''''. (* interactive def started *) - Parameter foo:nat. - End N''''. (* interactive def ended *) - End N'. + Declare Module N''':= N'. (* no interactive def started *) + Declare Module N''''. (* interactive def started *) + Parameter foo:nat. + End N''''. (* interactive def ended *) +End N'. - Lemma titi : O=O. - trivial. - Module Type K:=N'. - Module N''':=M. - Save. +Lemma titi : O=O. + trivial. + Module Type K:=N'. + Module N''':=M. +Save. - (* Here is a bug of Coq: *) - - Lemma bar:O=O. - Module Type L. (* This should not be allowed by Coq, since the End L. below fails *) - Axiom foo: O=O. - End L. (* fails --> if we go back to Module Type: unsync *) - Module I. - End I. + (* Here is a bug of Coq: *) +Lemma bar:O=O. + Module Type L. (* This should not be allowed by Coq, since the End L. below fails *) + Axiom foo: O=O. + End L. (* fails --> if we go back to Module Type: unsync *) + Module I. +End I. -- cgit v1.2.3