From 4a2b9073e61de1ab000b26652d94e63b382ce7d2 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 3 Dec 1999 16:23:22 +0000
Subject: bug make_strength repare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@200 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/astterm.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'parsing/astterm.ml')

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index b595c901f..7babfe020 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -428,14 +428,15 @@ let globalize_ast ast =
 
 
 (* Installation of the AST quotations. "command" is used by default. *)
-open Pcoq
-
 let _ = 
-  define_quotation true "command" (map_entry globalize_command Command.command)
+  Pcoq.define_quotation true "command" 
+    (Pcoq.map_entry globalize_command Pcoq.Command.command)
 let _ = 
-  define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic)
+  Pcoq.define_quotation false "tactic" 
+    (Pcoq.map_entry globalize_ast Pcoq.Tactic.tactic)
 let _ = 
-  define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac)
+  Pcoq.define_quotation false "vernac" 
+    (Pcoq.map_entry globalize_ast Pcoq.Vernac.vernac)
 
 
 (*********************************************************************)
-- 
cgit v1.2.3