aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-13 00:22:57 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-18 11:02:58 +0200
commit61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch)
treec0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /plugins/ssr
parentf08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff)
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrparser.ml46
-rw-r--r--plugins/ssr/ssrvernac.ml416
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