From 10621555f900d25df4fd2f71b045a050f8eb9f90 Mon Sep 17 00:00:00 2001
From: glondu
Date: Sat, 25 Dec 2010 19:25:42 +0000
Subject: Avoid "open {Pcoq,Extrawit}" clauses in expansion of EXTEND commands

It is quite nasty to insert those open in places where they can change
the semantics of surrounding code... instead, prefer using
fully-qualified names in generated code when possible. For
ExtraArgType, simulate a "open Extrawit in ..." (which does exist
primitively in OCaml >= 3.12) with the usual encoding.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13759 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/compat.ml4 | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/compat.ml4 b/lib/compat.ml4
index c95f7ed45d..d3f28b0570 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -189,11 +189,10 @@ END
 (** Fix a quotation difference in [str_item] *)
 
 let declare_str_items loc l =
-  let l' = <:str_item< open Pcoq >> :: <:str_item< open Extrawit >> :: l in
 IFDEF CAMLP5 THEN
-  MLast.StDcl (loc,l') (* correspond to <:str_item< declare $list:l'$ end >> *)
+  MLast.StDcl (loc,l) (* correspond to <:str_item< declare $list:l'$ end >> *)
 ELSE
-  Ast.stSem_of_list l'
+  Ast.stSem_of_list l
 END
 
 (** Quotation difference for match clauses *)
-- 
cgit v1.2.3