diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-22 18:09:11 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-22 18:09:11 +0000 |
| commit | 66ee7ba58080fa8fcfdb4bb76b89cc0b70a8a4ac (patch) | |
| tree | e97e3bd30fa49fc5da4dfe207ff73e841ee083b1 /parsing/g_vernac.ml4 | |
| parent | fe027346f901f26d79ce243a06c08a8c9f661e81 (diff) | |
traducteur: affiche les commentaires a l'interieur des commandes
extraction: pb avec les variables de section definies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index bda234764..d52ced817 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -33,6 +33,9 @@ let thm_token = G_proofs.thm_token (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) +let filter_com (b,e) = + Pp.comments := List.filter (fun ((b',e'),s) -> b'<b || e'>e) !Pp.comments + if !Options.v7 then GEXTEND Gram GLOBAL: vernac gallina_ext; @@ -49,7 +52,8 @@ GEXTEND Gram | "["; l = vernac_list_tail -> VernacList l (* For translation from V7 to V8 *) - | IDENT "V7only"; v = vernac -> VernacV7only v + | IDENT "V7only"; v = vernac -> + filter_com loc; VernacV7only v | IDENT "V8only"; v = vernac -> VernacV8only v (* |