diff options
| -rw-r--r-- | lib/compat.ml4 | 5 | ||||
| -rw-r--r-- | parsing/argextend.ml4 | 29 | ||||
| -rw-r--r-- | parsing/q_util.ml4 | 25 |
3 files changed, 36 insertions, 23 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 *) diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index dd4f2eb051..90116180eb 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -40,7 +40,12 @@ let rec make_rawwit loc = function | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >> | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >> + | ExtraArgType s -> + <:expr< + let module WIT = struct + open Extrawit; + value wit = $lid:"rawwit_"^s$; + end in WIT.wit >> let rec make_globwit loc = function | BoolArgType -> <:expr< Genarg.globwit_bool >> @@ -65,7 +70,12 @@ let rec make_globwit loc = function | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >> | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_globwit loc t1$ $make_globwit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"globwit_"^s$ >> + | ExtraArgType s -> + <:expr< + let module WIT = struct + open Extrawit; + value wit = $lid:"globwit_"^s$; + end in WIT.wit >> let rec make_wit loc = function | BoolArgType -> <:expr< Genarg.wit_bool >> @@ -90,24 +100,29 @@ let rec make_wit loc = function | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> | PairArgType (t1,t2) -> <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"wit_"^s$ >> + | ExtraArgType s -> + <:expr< + let module WIT = struct + open Extrawit; + value wit = $lid:"wit_"^s$; + end in WIT.wit >> let make_act loc act pil = let rec make = function - | [] -> <:expr< Gram.action (fun loc -> ($act$ : 'a)) >> + | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >> | GramNonTerminal (_,t,_,Some p) :: tl -> let p = Names.string_of_id p in <:expr< - Gram.action + Pcoq.Gram.action (fun $lid:p$ -> let _ = Genarg.in_gen $make_rawwit loc t$ $lid:p$ in $make tl$) >> | (GramTerminal _ | GramNonTerminal (_,_,_,None)) :: tl -> - <:expr< Gram.action (fun _ -> $make tl$) >> in + <:expr< Pcoq.Gram.action (fun _ -> $make tl$) >> in make (List.rev pil) let make_prod_item = function - | GramTerminal s -> <:expr< gram_token_of_string $str:s$ >> + | GramTerminal s -> <:expr< Pcoq.gram_token_of_string $str:s$ >> | GramNonTerminal (_,_,g,_) -> <:expr< Pcoq.symbol_of_prod_entry_key $mlexpr_of_prod_entry_key g$ >> diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 3a30701155..91ab29f1d4 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -52,19 +52,18 @@ let mlexpr_of_option f = function | Some e -> <:expr< Some $f e$ >> open Vernacexpr -open Pcoq open Genarg let rec mlexpr_of_prod_entry_key = function - | Alist1 s -> <:expr< Alist1 $mlexpr_of_prod_entry_key s$ >> - | Alist1sep (s,sep) -> <:expr< Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Alist0 s -> <:expr< Alist0 $mlexpr_of_prod_entry_key s$ >> - | Alist0sep (s,sep) -> <:expr< Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> - | Aopt s -> <:expr< Aopt $mlexpr_of_prod_entry_key s$ >> - | Amodifiers s -> <:expr< Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Aself -> <:expr< Aself >> - | Anext -> <:expr< Anext >> - | Atactic n -> <:expr< Atactic $mlexpr_of_int n$ >> - | Agram s -> Util.anomaly "Agram not supported" - | Aentry ("",s) -> <:expr< Agram (Gram.Entry.obj $lid:s$) >> - | Aentry (u,s) -> <:expr< Aentry $str:u$ $str:s$ >> + | Pcoq.Alist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> + | Pcoq.Alist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> + | Pcoq.Alist0 s -> <:expr< Pcoq.Alist0 $mlexpr_of_prod_entry_key s$ >> + | Pcoq.Alist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> + | Pcoq.Aopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> + | Pcoq.Amodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> + | Pcoq.Aself -> <:expr< Pcoq.Aself >> + | Pcoq.Anext -> <:expr< Pcoq.Anext >> + | Pcoq.Atactic n -> <:expr< Pcoq.Atactic $mlexpr_of_int n$ >> + | Pcoq.Agram s -> Util.anomaly "Agram not supported" + | Pcoq.Aentry ("",s) -> <:expr< Pcoq.Agram (Pcoq.Gram.Entry.obj $lid:s$) >> + | Pcoq.Aentry (u,s) -> <:expr< Pcoq.Aentry $str:u$ $str:s$ >> |