diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 18:49:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-17 18:49:35 +0000 |
| commit | 87919fe04edf32b367e8d6229e8f9d695b7e7a2e (patch) | |
| tree | a2609727709b97368298a811e84a3f6d99d0d3ab /translate | |
| parent | 3c2ea830b54564310342bc88376e66281d0b4bde (diff) | |
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et VERNAC EXTEND (e.g. Hint Rewrite) [2eme]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5526 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppvernacnew.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index c7b7acf57..9c80e0afe 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -1059,7 +1059,6 @@ and pr_extend s cl = try (* Hack pour les syntaxes changeant non uniformément en passant a la V8 *) let s = - print_string s; flush stdout; let n = String.length s in if Options.do_translate() & n > 2 & String.sub s (n-2) 2 = "V7" then String.sub s 0 (n-2) ^ "V8" |