diff options
| author | herbelin | 2002-12-10 09:38:39 +0000 |
|---|---|---|
| committer | herbelin | 2002-12-10 09:38:39 +0000 |
| commit | 4affad97b01e15ccfb96a3a6a8c24964dbb4320d (patch) | |
| tree | 96c925dc17755278ff596b8a32d779f9a5799752 /parsing | |
| parent | b094efba69a0289db5b431ef939bab124936b06d (diff) | |
Ajout options -v7 et -v8, et commandes V7only et V8only
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3407 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 30c0d368be..57d799a15c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -41,8 +41,16 @@ GEXTEND Gram | c = syntax; "." -> c | n = natural; ":"; v = goal_vernac; "." -> v n | "["; l = vernac_list_tail -> VernacList l + + (* For translation from V7 to V8 *) + | IDENT "V7only"; v = vernac -> VernacV7only v + | IDENT "V8only"; v = vernac -> VernacV8only v + +(* (* This is for "Grammar vernac" rules *) - | id = METAIDENT -> VernacVar (Names.id_of_string id) ] ] + | id = METAIDENT -> VernacVar (Names.id_of_string id) +*) + ] ] ; goal_vernac: [ [ tac = Tactic.tactic -> fun n -> VernacSolve (n,tac) |