From fd1088cfa83a01d9139bd7bbdd112cdff4ca1b9a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 20 Sep 2001 14:16:56 +0000
Subject: bug affichage des termes ml fournis

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2022 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/ocaml.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 71c32d215b..1bc47b1e0d 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -443,10 +443,10 @@ module ModularParams = struct
   let rename_global r = id_of_string (rename_global_aux r)
 
   let pp_type_global r = 
-    string ((module_option r)^(check_ml r (rename_type_global r)))
+    string (check_ml r ((module_option r)^(rename_type_global r)))
 
   let pp_global r = 
-    string ((module_option r)^(check_ml r (rename_global_aux r)))
+    string (check_ml r ((module_option r)^(rename_global_aux r)))
 
   let cofix_warning = true
 end
-- 
cgit v1.2.3