diff options
Diffstat (limited to 'plugins/ssr/ssrvernac.ml4')
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 38 |
1 files changed, 18 insertions, 20 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 05dbf0a8..989a6c5b 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -19,17 +19,14 @@ open Constrexpr_ops open Pcoq open Pcoq.Prim open Pcoq.Constr -open Pcoq.Vernac_ +open Pvernac.Vernac_ open Ltac_plugin open Notation_ops open Notation_term open Glob_term -open Globnames open Stdarg open Genarg -open Misctypes open Decl_kinds -open Libnames open Pp open Ppconstr open Printer @@ -144,21 +141,21 @@ END let declare_one_prenex_implicit locality f = let fref = try Smartlocate.global_with_alias f - with _ -> errorstrm (pr_reference f ++ str " is not declared") in + with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> - errorstrm (str "Expected prenex implicits for " ++ pr_reference f) + errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in let impls = match Impargs.implicits_of_global fref with | [cond,impls] -> impls - | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f) + | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | _ -> errorstrm (str "Multiple implicits not supported") in match loop impls with | [] -> - errorstrm (str "Expected some implicits for " ++ pr_reference f) + errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] @@ -220,8 +217,8 @@ let interp_search_notation ?loc tag okey = (Bytes.set s' i' '_'; loop (j + 1) (i' + 2)) else (String.blit s i s' i' m; loop (j + 1) (i' + m + 1)) in loop 0 1 in - let trim_ntn (pntn, m) = Bytes.sub_string pntn 1 (max 0 m) in - let pr_ntn ntn = str "(" ++ str ntn ++ str ")" in + let trim_ntn (pntn, m) = (InConstrEntrySomeLevel,Bytes.sub_string pntn 1 (max 0 m)) in + let pr_ntn ntn = str "(" ++ Notation.pr_notation ntn ++ str ")" in let pr_and_list pr = function | [x] -> pr x | x :: lx -> pr_list pr_comma pr lx ++ pr_comma () ++ str "and " ++ pr x @@ -296,7 +293,7 @@ let interp_search_notation ?loc tag okey = let scs' = List.remove (=) sc !scs in let w = pr_ntn ntn ++ str " is also defined " ++ pr_scs scs' in Feedback.msg_warning (hov 4 w) - else if String.string_contains ~where:ntn ~what:" .. " then + else if String.string_contains ~where:(snd ntn) ~what:" .. " then err (pr_ntn ntn ++ str " is an n-ary notation"); let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in let rec sub () = function @@ -361,13 +358,12 @@ let coerce_search_pattern_to_sort hpat = true, cp with _ -> false, [] in let coerce hp coe_index = - let coe = Classops.get_coercion_value coe_index in + let coe_ref = coe_index.Classops.coe_value in try - let coe_ref = global_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] - with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () + with Not_found | Option.IsNone -> + errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path @@ -377,7 +373,10 @@ let interp_head_pat hpat = | Cast (c', _, _) -> loop c' | Prod (_, _, c') -> loop c' | LetIn (_, _, _, c') -> loop c' - | _ -> Constr_matching.is_matching (Global.env()) Evd.empty p (EConstr.of_constr c) in + | _ -> + let env = Global.env () in + let sigma = Evd.from_env env in + Constr_matching.is_matching env sigma p (EConstr.of_constr c) in filter_head, loop let all_true _ = true @@ -413,7 +412,7 @@ let interp_search_arg arg = (* Module path postfilter *) -let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m +let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc @@ -431,10 +430,9 @@ GEXTEND Gram END let interp_modloc mr = - let interp_mod (_, mr) = - let {CAst.loc=loc; v=qid} = qualid_of_reference mr in + let interp_mod (_, qid) = try Nametab.full_name_module qid with Not_found -> - CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in + CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in let interp_bmod b = function | [] -> fun _ _ _ -> true |