[ssreflect] Better use of Coqlib

 - Look constants up using registered names
 - As lazily as possible

4 files changed, 29 insertions, 12 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 6746eff223..12f1664b4d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -730,13 +730,10 @@ let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project
 (** look up a name in the ssreflect internals module *)
 let ssrdirpath = DirPath.make [Id.of_string "ssreflect"]
 let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) 
-let ssrtopqid name = Libnames.qualid_of_ident (Id.of_string name) 
-let locate_reference qid =
-  Smartlocate.global_of_extended_global (Nametab.locate_extended qid)
 let mkSsrRef name =
-  try locate_reference (ssrqid name) with Not_found ->
-  try locate_reference (ssrtopqid name) with Not_found ->
-  CErrors.user_err (Pp.str "Small scale reflection library not loaded")
+  let qn = Format.sprintf "plugins.ssreflect.%s" name in
+  if Coqlib.has_ref qn then Coqlib.lib_ref qn else
+  CErrors.user_err Pp.(str "Small scale reflection library not loaded (" ++ str name ++ str ")")
 let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None
 let mkSsrConst name env sigma =
   EConstr.fresh_global env sigma (mkSsrRef name)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 9ba23467e7..566a933522 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -212,8 +212,7 @@ val pf_abs_prod :
            EConstr.t -> Goal.goal Evd.sigma * EConstr.types
 
 val mkSsrRRef : string -> Glob_term.glob_constr * 'a option
-val mkSsrRef : string -> GlobRef.t
-val mkSsrConst : 
+val mkSsrConst :
            string ->
            env -> evar_map -> evar_map * EConstr.t
 val pf_mkSsrConst :
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 460bdc6d23..e43cab094b 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -159,6 +159,10 @@ Definition abstract (statement : Type) (id : nat) (lock : abstract_lock) :=
 Notation "<hidden n >" := (abstract _ n _).
 Notation "T (* n *)" := (abstract T n abstract_key).
 
+Register abstract_lock as plugins.ssreflect.abstract_lock.
+Register abstract_key as plugins.ssreflect.abstract_key.
+Register abstract as plugins.ssreflect.abstract.
+
 (* Constants for tactic-views *)
 Inductive external_view : Type := tactic_view of Type.
 
@@ -287,6 +291,8 @@ Variant phant (p : Type) := Phant.
 
 Definition protect_term (A : Type) (x : A) : A := x.
 
+Register protect_term as plugins.ssreflect.protect_term.
+
 (* The ssreflect idiom for a non-keyed pattern:                               *)
 (*  - unkeyed t wiil match any subterm that unifies with t, regardless of     *)
 (*    whether it displays the same head symbol as t.                          *)
@@ -336,6 +342,9 @@ Notation nosimpl t := (let: tt := tt in t).
 Lemma master_key : unit. Proof. exact tt. Qed.
 Definition locked A := let: tt := master_key in fun x : A => x.
 
+Register master_key as plugins.ssreflect.master_key.
+Register locked as plugins.ssreflect.locked.
+
 Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
 
 (* Needed for locked predicates, in particular for eqType's.                  *)
@@ -395,12 +404,18 @@ Definition ssr_have_let Pgoal Plemma step
   (rest : let x : Plemma := step in Pgoal) : Pgoal := rest.
 Arguments ssr_have_let [Pgoal].
 
+Register ssr_have as plugins.ssreflect.ssr_have.
+Register ssr_have_let as plugins.ssreflect.ssr_have_let.
+
 Definition ssr_suff Plemma Pgoal step (rest : Plemma) : Pgoal := step rest.
 Arguments ssr_suff Plemma [Pgoal].
 
 Definition ssr_wlog := ssr_suff.
 Arguments ssr_wlog Plemma [Pgoal].
 
+Register ssr_suff as plugins.ssreflect.ssr_suff.
+Register ssr_wlog as plugins.ssreflect.ssr_wlog.
+
 (* Internal N-ary congruence lemmas for the congr tactic.                     *)
 
 Fixpoint nary_congruence_statement (n : nat)
@@ -425,6 +440,9 @@ Lemma ssr_congr_arrow Plemma Pgoal : Plemma = Pgoal -> Plemma -> Pgoal.
 Proof. by move->. Qed.
 Arguments ssr_congr_arrow : clear implicits.
 
+Register nary_congruence as plugins.ssreflect.nary_congruence.
+Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow.
+
 (* View lemmas that don't use reflection.                                     *)
 
 Section ApplyIff.
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 7f9a9e125e..5067d8af31 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -16,7 +16,6 @@ open Printer
 open Term
 open Constr
 open Termops
-open Globnames
 open Tactypes
 open Tacmach
 
@@ -98,6 +97,11 @@ let subgoals_tys sigma (relctx, concl) =
  *    generalize the equality in case eqid is not None
  * 4. build the tactic handle intructions and clears as required in ipats and
  *    by eqid *)
+
+let get_eq_type gl =
+  let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
+  gl, EConstr.of_constr eq
+
 let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac gl =
   (* some sanity checks *)
   let oc, orig_clr, occ, c_gen, gl = match what with
@@ -115,8 +119,6 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
   let orig_gl, concl, env = gl, pf_concl gl, pf_env gl in
   ppdebug(lazy(Pp.str(if is_case then "==CASE==" else "==ELIM==")));
   let fire_subst gl t = Reductionops.nf_evar (project gl) t in
-  let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
-  let eq = EConstr.of_constr eq in
   let is_undef_pat = function
   | sigma, T t -> EConstr.isEvar sigma (EConstr.of_constr t)
   | _ -> false in
@@ -322,6 +324,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
         let k = List.length deps in
         let c = fire_subst gl (List.assoc (n_elim_args - k - 1) elim_args) in
         let gl, t = pfe_type_of gl c in
+        let gl, eq = get_eq_type gl in
         let gen_eq_tac, gl =
           let refl = EConstr.mkApp (eq, [|t; c; c|]) in
           let new_concl = EConstr.mkArrow refl (EConstr.Vars.lift 1 (pf_concl orig_gl)) in 
@@ -421,7 +424,7 @@ let injectl2rtac sigma c = match EConstr.kind sigma c with
 let is_injection_case c gl =
   let gl, cty = pfe_type_of gl c in
   let (mind,_), _ = pf_reduce_to_quantified_ind gl cty in
-  GlobRef.equal (IndRef mind) Coqlib.(lib_ref "core.eq.type")
+  Coqlib.check_ind_ref "core.eq.type" mind
 
 let perform_injection c gl =
   let gl, cty = pfe_type_of gl c in