aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib7
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-29 20:02:41 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-11-29 20:02:41 +0000
commit301d935ead634951485e3f3394576611e6a56659 (patch)
tree3693a1147ba6cd820223b421b8510c267a8870c7 /contrib7
parentc78e5075c51975e828d83a240892114ea741fbca (diff)
Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5038 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib7')
-rw-r--r--contrib7/.cvsignore1
-rw-r--r--contrib7/extraction/.cvsignore1
-rw-r--r--contrib7/interface/vernacrc17
3 files changed, 19 insertions, 0 deletions
diff --git a/contrib7/.cvsignore b/contrib7/.cvsignore
new file mode 100644
index 000000000..7835a7915
--- /dev/null
+++ b/contrib7/.cvsignore
@@ -0,0 +1 @@
+why
diff --git a/contrib7/extraction/.cvsignore b/contrib7/extraction/.cvsignore
new file mode 100644
index 000000000..c446fcb87
--- /dev/null
+++ b/contrib7/extraction/.cvsignore
@@ -0,0 +1 @@
+*.v8
diff --git a/contrib7/interface/vernacrc b/contrib7/interface/vernacrc
new file mode 100644
index 000000000..b66f1e4c1
--- /dev/null
+++ b/contrib7/interface/vernacrc
@@ -0,0 +1,17 @@
+# $Id$
+
+# This file is loaded initially by ./vernacparser.
+
+load_syntax_file 17 LogicSyntax
+load_syntax_file 36 SpecifSyntax
+load_syntax_file 18 Logic_TypeSyntax
+load_syntax_file 19 DatatypesSyntax
+load_syntax_file 21 Equality
+load_syntax_file 22 Inv
+load_syntax_file 26 Tauto
+load_syntax_file 34 Omega
+load_syntax_file 27 Ring
+quiet_parse_string
+Goal a.
+&& END--OF--DATA
+print_version