diff options
| author | herbelin | 2004-03-17 18:49:35 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-17 18:49:35 +0000 |
| commit | 87919fe04edf32b367e8d6229e8f9d695b7e7a2e (patch) | |
| tree | a2609727709b97368298a811e84a3f6d99d0d3ab | |
| 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
| -rw-r--r-- | parsing/pptactic.ml | 1 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 41f7ba954c..fc44758bef 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -406,7 +406,6 @@ let pr_extend_gen prgen s l = let tags = List.map genarg_tag l in (* 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" diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index c7b7acf57f..9c80e0afe8 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" |