aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-21 23:22:00 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-21 23:22:00 +0000
commit03472e2da94043fa35a618e92191b63fbe4c196d (patch)
treed3e08f372afdc062bb71129dd9592fb89c9ee3a6
parent4a5523694f0b3da2b6c7e6ee7a4b03dc402d4205 (diff)
MAJ syntaxe v7 avant activation en syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7689 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--test-suite/modules/mod_decl.v18
-rw-r--r--test-suite/modules/modeq.v2
-rw-r--r--test-suite/modules/modul.v8
-rw-r--r--test-suite/modules/sig.v2
4 files changed, 11 insertions, 19 deletions
diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v
index 867b8a11f..a9d22d79d 100644
--- a/test-suite/modules/mod_decl.v
+++ b/test-suite/modules/mod_decl.v
@@ -1,5 +1,4 @@
Module Type SIG.
- Definition A:Set. (*error*)
Axiom A:Set.
End SIG.
@@ -27,13 +26,9 @@ Module M5<:SIG:=M0.
Module F[X:SIG]:=X.
-Declare Module M6.
-
-
Module Type T.
- Declare Module M0.
- Lemma A:Set (*error*).
+ Module M0.
Axiom A:Set.
End M0.
@@ -43,13 +38,12 @@ Module Type T.
Definition A:=nat.
End M2.
- Declare Module M3:=M0.
+ Module M3:=M0.
- Declare Module M4:SIG:=M0. (* error *)
+ Module M4:SIG:=M0.
- Declare Module M5<:SIG:=M0.
+ Module M5<:SIG:=M0.
- Declare Module M6:=F M0. (* error *)
+ Module M6:=F M0.
- Module M7.
-End T. \ No newline at end of file
+End T.
diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v
index 73448dc7f..9e74a310d 100644
--- a/test-suite/modules/modeq.v
+++ b/test-suite/modules/modeq.v
@@ -4,7 +4,7 @@ Module M.
End M.
Module Type SIG.
- Declare Module M:=Top.M.
+ Module M:=Top.M.
Module Type SIG.
Parameter T:Set.
End SIG.
diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v
index 5612ea755..58ae2a52d 100644
--- a/test-suite/modules/modul.v
+++ b/test-suite/modules/modul.v
@@ -16,24 +16,22 @@ Module M.
End M.
+Locate Module M.
+
(*Lemma w1 : (M.rel O (S O)).
Auto.
*)
Import M.
-Print Hint *.
Lemma w1 : (O#(S O)).
-Print Hint.
-Print Hint *.
-
Auto.
Save.
Check (O#O).
Locate rel.
-Locate M.
+Locate Module M.
Module N:=Top.M.
diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v
index eb8736bba..c09a74324 100644
--- a/test-suite/modules/sig.v
+++ b/test-suite/modules/sig.v
@@ -12,7 +12,7 @@ End M.
Module N:=M.
Module Type SPRYT.
- Declare Module N.
+ Module N.
Definition T:=M.N.T.
Parameter x:T.
End N.