From 8ba99b2013e0f62c9117fc79364630ff1fbec585 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 26 Apr 2006 22:31:52 +0000 Subject: Changed the type of proof-goal-command-p. It takes now a span, which allows using a span attribute to detect goal commands. I think I modified all modes accordingly. --- coq/ex-module.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'coq/ex-module.v') diff --git a/coq/ex-module.v b/coq/ex-module.v index 5b9d638a..413a4966 100644 --- a/coq/ex-module.v +++ b/coq/ex-module.v @@ -28,6 +28,10 @@ Module M. Parameter T:Set. Parameter x:T. End SIG. + Module Type SIG'. + Parameter T:Set. + Parameter x:T. + End SIG'. Lemma toto : O=O. Definition t:=nat. trivial. @@ -66,16 +70,13 @@ Module Type N'. Module Type M'. Declare Module K:N.SIG. End M'. - Declare Module N''. +(* Declare Module N''. *) Definition T:=nat. Definition x:=O. - End 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 *) + Declare Module N''' :M.SIG. (* no interactive def started *) End N'. @@ -90,7 +91,6 @@ Save. 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