diff options
Diffstat (limited to 'plugins/ssr')
-rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrparser.ml4 | 6 | ||||
-rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 16 |
3 files changed, 12 insertions, 12 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 2a31157be..54f3f9c71 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -858,7 +858,7 @@ open Util (** Constructors for constr_expr *) let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) -let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) +let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 352f88bb3..7a1d06fdc 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1154,7 +1154,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id + | { v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c @@ -1246,7 +1247,8 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc (qualid_basename qid) | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 939e97866..7ce2dd64a 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -28,7 +28,6 @@ open Globnames open Stdarg open Genarg open Decl_kinds -open Libnames open Pp open Ppconstr open Printer @@ -143,21 +142,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] @@ -415,7 +414,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 @@ -433,10 +432,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 |