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 /parsing/pptactic.ml | |
| 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 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 41f7ba954..fc44758be 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" |