diff options
Diffstat (limited to 'mathcomp/ssreflect/plugin/trunk')
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 39 |
1 files changed, 20 insertions, 19 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 index ee13c15..93a1ba7 100644 --- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 @@ -29,7 +29,7 @@ open Pcoq.Prim open Pcoq.Constr open Genarg open Stdarg -open Constrarg +open Tacarg open Term open Vars open Context @@ -45,6 +45,7 @@ open Coqlib open Glob_term open Util open Evd +open Proofview.Notations open Sigma.Notations open Extend open Goptions @@ -52,7 +53,7 @@ open Tacexpr open Tacinterp open Pretyping open Constr -open Tactic +open Pltac open Extraargs open Ppconstr open Printer @@ -99,8 +100,8 @@ module Intset = Evar.Set type loc = Loc.t let dummy_loc = Loc.ghost -let errorstrm = CErrors.errorlabstrm "ssreflect" -let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg) +let errorstrm msg = CErrors.user_err ~hdr:"ssreflect" msg +let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg) let anomaly s = CErrors.anomaly (str s) (* Compatibility with Coq 8.6 *) @@ -471,7 +472,7 @@ let _ = Goptions.optwrite = (fun _ -> Lib.add_anonymous_leaf (inVersion ssrAstVersion)) } -let tactic_expr = Tactic.tactic_expr +let tactic_expr = Pltac.tactic_expr let gallina_ext = Vernac_.gallina_ext let sprintf = Printf.sprintf let tactic_mode = G_ltac.tactic_mode @@ -1138,7 +1139,7 @@ let interp_view_nbimps ist gl rc = let si = sig_it gl in let gl = re_sig si sigma in let pl, c = splay_open_constr gl t in - if isAppInd gl c then List.length pl else ~-(List.length pl) + if isAppInd gl c then List.length pl else (-(List.length pl)) with _ -> 0 (* }}} *) @@ -1222,7 +1223,7 @@ let interp_search_notation loc s opt_scope = let ambig = "This string refers to a complex or ambiguous notation." in str ambig ++ str "\nTry searching with one of\n" ++ ntns with _ -> str "This string is not part of an identifier or notation." in - CErrors.user_err_loc (loc, "interp_search_notation", diagnosis) + CErrors.user_err ~loc ~hdr:"interp_search_notation" diagnosis let pr_ssr_search_item _ _ _ = pr_search_item @@ -1233,7 +1234,7 @@ let is_ident s = try CLexer.check_ident s; true with _ -> false let is_ident_part s = is_ident ("H" ^ s) let interp_search_notation loc tag okey = - let err msg = CErrors.user_err_loc (loc, "interp_search_notation", msg) in + let err msg = CErrors.user_err ~loc ~hdr:"interp_search_notation" msg in let mk_pntn s for_key = let n = String.length s in let s' = String.make (n + 2) ' ' in @@ -1454,7 +1455,7 @@ let interp_modloc mr = let interp_mod (_, mr) = let (loc, qid) = qualid_of_reference mr in try Nametab.full_name_module qid with Not_found -> - CErrors.user_err_loc (loc, "interp_modloc", str "No Module " ++ pr_qualid qid) in + CErrors.user_err ~loc ~hdr:"interp_modloc" (str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in let interp_bmod b = function | [] -> fun _ _ _ -> true @@ -1465,7 +1466,7 @@ let interp_modloc mr = (* The unified, extended vernacular "Search" command *) let ssrdisplaysearch gr env t = - let pr_res = pr_global gr ++ spc () ++ str " " ++ pr_lconstr_env env Evd.empty t in + let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in msg_info (hov 2 pr_res ++ fnl ()) VERNAC COMMAND EXTEND SsrSearchPattern CLASSIFIED AS QUERY @@ -1760,7 +1761,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp let hyp_err loc msg id = - CErrors.user_err_loc (loc, "ssrhyp", str msg ++ pr_id id) + CErrors.user_err ~loc ~hdr:"ssrhyp" (str msg ++ pr_id id) let intern_hyp ist (SsrHyp (loc, id) as hyp) = let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in @@ -2084,8 +2085,8 @@ let abs_wgen keep_let ist f gen (gl,args,c) = let sigma, env = project gl, pf_env gl in let evar_closed t p = if occur_existential t then - CErrors.user_err_loc (loc_of_cpattern p,"ssreflect", - pr_constr_pat t ++ + CErrors.user_err ~loc:(loc_of_cpattern p) ~hdr:"ssreflect" + (pr_constr_pat t ++ str" contains holes and matches no subterm of the goal") in match gen with | _, Some ((x, mode), None) when mode = "@" || (mode = " " && keep_let) -> @@ -2689,7 +2690,7 @@ END (* subsets of patterns *) let check_ssrhpats loc w_binders ipats = - let err_loc s = CErrors.user_err_loc (loc, "ssreflect", s) in + let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in let clr, ipats = let rec aux clr = function | IpatSimpl (cl, Nop) :: tl -> aux (clr @ cl) tl @@ -5703,7 +5704,7 @@ ARGUMENT EXTEND ssrhavefwdwbinders tr, ((((clr, pats), allbinders), simpl), hint) ] END -(* Tactic. *) +(* Pltac. *) let is_Evar_or_CastedMeta x = isEvar_or_Meta x || @@ -6205,8 +6206,8 @@ END (* longer and thus comment out. Such comments are marked with v8.3 *) GEXTEND Gram - GLOBAL: Tactic.hypident; - Tactic.hypident: [ + GLOBAL: Pltac.hypident; + Pltac.hypident: [ [ "("; IDENT "type"; "of"; id = Prim.identref; ")" -> id, InHypTypeOnly | "("; IDENT "value"; "of"; id = Prim.identref; ")" -> id, InHypValueOnly ] ]; @@ -6223,8 +6224,8 @@ hloc: [ END GEXTEND Gram - GLOBAL: Tactic.constr_eval; - Tactic.constr_eval: [ + GLOBAL: Pltac.constr_eval; + Pltac.constr_eval: [ [ IDENT "type"; "of"; c = Constr.constr -> Genredexpr.ConstrTypeOf c ] ]; END |