diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d21223d43d..4d55946336 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -15,11 +15,13 @@ let frozen_lexer = CLexer.freeze () ;; (*i camlp4use: "pa_extend.cmo" i*) (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Names open Pp open Pcoq open Genarg -open Constrarg +open Stdarg +open Tacarg open Term open Vars open Topconstr @@ -41,7 +43,7 @@ open Proofview.Notations open Tacinterp open Pretyping open Constr -open Tactic +open Pltac open Extraargs open Ppconstr open Printer @@ -61,8 +63,8 @@ DECLARE PLUGIN "ssrmatching_plugin" type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = CErrors.errorlabstrm "ssrmatching" -let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg) +let errorstrm = CErrors.user_err ~hdr:"ssrmatching" +let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) @@ -154,7 +156,7 @@ let mkCHole loc = CHole (loc, None, IntroAnonymous, None) let mkCLambda loc name ty t = CLambdaN (loc, [[loc, name], Default Explicit, ty], t) let mkCLetIn loc name bo t = - CLetIn (loc, (loc, name), bo, t) + CLetIn (loc, (loc, name), bo, None, t) let mkCCast loc t ty = CCast (loc,t, dC ty) (** Constructors for rawconstr *) let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None) @@ -1191,7 +1193,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b)) - | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in + | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t @@ -1410,7 +1412,7 @@ let () = let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = - TacFun ([Some (Id.of_string "pattern")], + TacFun ([Name (Id.of_string "pattern")], TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in let obj () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in |