diff options
| author | glondu | 2010-12-25 19:25:42 +0000 |
|---|---|---|
| committer | glondu | 2010-12-25 19:25:42 +0000 |
| commit | 10621555f900d25df4fd2f71b045a050f8eb9f90 (patch) | |
| tree | f1b173e44dabcf1810fbc733b2a020aa0dfb3a85 /lib | |
| parent | 2c6c48388fa5ce84d66eb92fd9574951628a2c34 (diff) | |
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
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/compat.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
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 *) |