Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Defined constants

Reviewed-by: ppedrot

2 files changed, 31 insertions, 6 deletions

diff --git a/test-suite/bugs/closed/bug_12566_1.v b/test-suite/bugs/closed/bug_12566_1.v
new file mode 100644
index 0000000000..22d95949bb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12566_1.v
@@ -0,0 +1,16 @@
+
+Class C (n:nat) := c{}.
+
+Instance c0 : C 0 := {}.
+
+Definition x := 0.
+
+Opaque x.
+
+Type _ : C x.
+(* this is maybe wrong behaviour, if it changes just update the test *)
+
+Hint Opaque x : typeclass_instances.
+Transparent x.
+
+Fail Type _ : C x.
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 0e3e3c61a9..051560fb63 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Util
+open Names
 
 (** (Partial) implementation of the [Hint] command; some more
    functionality still lives in tactics/hints.ml *)
@@ -61,7 +62,7 @@ let project_hint ~poly pri l2r r =
       cb
   in
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-  (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c))
+  (info, false, true, Hints.PathAny, Hints.IsGlobRef (GlobRef.ConstRef c))
 
 let warn_deprecated_hint_constr =
   CWarnings.create ~name:"fragile-hint-constr" ~category:"automation"
@@ -70,6 +71,16 @@ let warn_deprecated_hint_constr =
         "Declaring arbitrary terms as hints is fragile; it is recommended to \
          declare a toplevel constant instead")
 
+(* Only error when we have to (axioms may be instantiated if from functors)
+   XXX maybe error if not from a functor argument?
+ *)
+let soft_evaluable =
+  let open GlobRef in
+  function
+  | ConstRef c -> EvalConstRef c
+  | VarRef id -> EvalVarRef id
+  | (IndRef _ | ConstructRef _) as r -> Tacred.error_not_evaluable r
+
 let interp_hints ~poly h =
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -88,7 +99,7 @@ let interp_hints ~poly h =
     Dumpglob.add_glob ?loc:r.CAst.loc gr;
     gr
   in
-  let fr r = Tacred.evaluable_of_global_reference env (fref r) in
+  let fr r = soft_evaluable (fref r) in
   let fi c =
     let open Hints in
     let open Vernacexpr in
@@ -135,7 +146,7 @@ let interp_hints ~poly h =
         "ind";
       List.init (Inductiveops.nconstructors env ind) (fun i ->
           let c = (ind, i + 1) in
-          let gr = Names.GlobRef.ConstructRef c in
+          let gr = GlobRef.ConstructRef c in
           ( empty_hint_info
           , Declareops.inductive_is_polymorphic mib
           , true
@@ -147,9 +158,7 @@ let interp_hints ~poly h =
     let pat = Option.map (fp sigma) patcom in
     let l = match pat with None -> [] | Some (l, _) -> l in
     let ltacvars =
-      List.fold_left
-        (fun accu x -> Names.Id.Set.add x accu)
-        Names.Id.Set.empty l
+      List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l
     in
     let env = Genintern.{(empty_glob_sign env) with ltacvars} in
     let _, tacexp = Genintern.generic_intern env tacexp in