diff options
Diffstat (limited to 'grammar/argextend.mlp')
| -rw-r--r-- | grammar/argextend.mlp | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index cc92680fc..643b6277a 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -46,17 +46,17 @@ let make_act loc act pil = make (List.rev pil) let make_prod_item = function - | ExtTerminal s -> <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $mlexpr_of_string s$) >> + | ExtTerminal s -> <:expr< Extend.Atoken (CLexer.terminal $mlexpr_of_string s$) >> | ExtNonTerminal (g, _) -> let base s = <:expr< $lid:s$ >> in mlexpr_of_prod_entry_key base g let rec make_prod = function -| [] -> <:expr< Grammar_API.Extend.Stop >> -| item :: prods -> <:expr< Grammar_API.Extend.Next $make_prod prods$ $make_prod_item item$ >> +| [] -> <:expr< Extend.Stop >> +| item :: prods -> <:expr< Extend.Next $make_prod prods$ $make_prod_item item$ >> let make_rule loc (prods,act) = - <:expr< Grammar_API.Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> + <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> let is_ident x = function | <:expr< $lid:s$ >> -> (s : string) = x @@ -67,7 +67,7 @@ let make_extend loc s cl wit = match cl with (** Special handling of identity arguments by not redeclaring an entry *) <:str_item< value $lid:s$ = - let () = Grammar_API.Pcoq.register_grammar $wit$ $lid:e$ in + let () = Pcoq.register_grammar $wit$ $lid:e$ in $lid:e$ >> | _ -> @@ -75,8 +75,8 @@ let make_extend loc s cl wit = match cl with let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< value $lid:s$ = - let $lid:s$ = Grammar_API.Pcoq.create_generic_entry Grammar_API.Pcoq.utactic $se$ (Genarg.rawwit $wit$) in - let () = Grammar_API.Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in + let $lid:s$ = Pcoq.create_generic_entry Pcoq.utactic $se$ (Genarg.rawwit $wit$) in + let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in $lid:s$ >> let warning_redundant prefix s = @@ -127,7 +127,7 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = begin match globtyp with | None -> let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in - <:expr< fun ist v -> API.Ftactic.return (API.Geninterp.Val.inject (API.Geninterp.val_tag $make_topwit loc typ$) v) >> + <:expr< fun ist v -> Ftactic.return (Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v) >> | Some globtyp -> <:expr< fun ist x -> Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x) >> @@ -137,10 +137,10 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in <:expr< let f = $lid:f$ in - fun ist v -> API.Ftactic.nf_enter (fun gl -> - let (sigma, v) = API.Tacmach.New.of_old (fun gl -> f ist gl v) gl in - let v = API.Geninterp.Val.inject (API.Geninterp.val_tag $make_topwit loc typ$) v in - API.Proofview.tclTHEN (API.Proofview.Unsafe.tclEVARS sigma) (API.Ftactic.return v) + fun ist v -> Ftactic.nf_enter (fun gl -> + let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in + let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v) ) >> in let subst = match h with @@ -156,15 +156,15 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = | Some f -> <:expr< $lid:f$>> in let dyn = match typ with | None -> <:expr< None >> - | Some typ -> <:expr< Some (API.Geninterp.val_tag $make_topwit loc typ$) >> + | Some typ -> <:expr< Some (Geninterp.val_tag $make_topwit loc typ$) >> in let wit = <:expr< $lid:"wit_"^s$ >> in declare_str_items loc [ <:str_item< value ($lid:"wit_"^s$) = Genarg.make0 $se$ >>; - <:str_item< Grammar_API.Genintern.register_intern0 $wit$ $glob$ >>; - <:str_item< Grammar_API.Genintern.register_subst0 $wit$ $subst$ >>; - <:str_item< API.Geninterp.register_interp0 $wit$ $interp$ >>; - <:str_item< API.Geninterp.register_val0 $wit$ $dyn$ >>; + <:str_item< Genintern.register_intern0 $wit$ $glob$ >>; + <:str_item< Genintern.register_subst0 $wit$ $subst$ >>; + <:str_item< Geninterp.register_interp0 $wit$ $interp$ >>; + <:str_item< Geninterp.register_val0 $wit$ $dyn$ >>; make_extend loc s cl wit; <:str_item< do { Pptactic.declare_extra_genarg_pprule |