diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-14 14:52:59 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-14 14:52:59 +0000 |
| commit | a0048524c33e113fc7549cd4248e4badcee4164d (patch) | |
| tree | 603f9cd5c86510319fbfe734fde3855ed60528b3 /contrib/interface | |
| parent | c53d8648b40d329a99ca7e0ef12c4d276ac716c8 (diff) | |
Now, the grammar extension from .v files are concentrated in just a few
files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5202 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/vernacrc | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/contrib/interface/vernacrc b/contrib/interface/vernacrc index b66f1e4c1..14f7e8c98 100644 --- a/contrib/interface/vernacrc +++ b/contrib/interface/vernacrc @@ -2,13 +2,8 @@ # 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 1 Notations +load_syntax_file 2 Logic load_syntax_file 34 Omega load_syntax_file 27 Ring quiet_parse_string |