Move the static check of evaluability in unfold tactic to runtime.

See #11840 for a motivation. I had to fix Floats.FloatLemmas because
it uses the same name for a notation and a term, and the fact this
unfold was working on this was clearly a bug. I hope nobody relies
on this kind of stuff in the wild.

Fixes #5764: "Cannot coerce ..." should be a runtime error.
Fixes #5159: "Cannot coerce ..." should not be an error.
Fixes #4925: unfold gives error on Admitted.

6 files changed, 68 insertions, 52 deletions

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 1aa3af0087..ff1e8b92d1 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -14,7 +14,6 @@ open CAst
 open Pattern
 open Genredexpr
 open Glob_term
-open Tacred
 open Util
 open Names
 open Libnames
@@ -294,23 +293,30 @@ let intern_destruction_arg ist = function
       else
         clear,ElimOnIdent (make ?loc id)
 
-let short_name = function
-  | {v=AN qid} when qualid_is_ident qid && not !strict_check ->
+let short_name qid =
+  if qualid_is_ident qid && not !strict_check then
     Some (make ?loc:qid.CAst.loc @@ qualid_basename qid)
-  | _ -> None
-
-let intern_evaluable_global_reference ist qid =
-  try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid)
-  with Not_found ->
-  if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid)
-  else Nametab.error_global_not_found qid
-
-let intern_evaluable_reference_or_by_notation ist = function
-  | {v=AN r} -> intern_evaluable_global_reference ist r
+  else None
+
+let evalref_of_globref ?loc ?short = function
+  | GlobRef.ConstRef cst -> ArgArg (EvalConstRef cst, short)
+  | GlobRef.VarRef id -> ArgArg (EvalVarRef id, short)
+  | r ->
+    user_err ?loc (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
+     spc () ++ str "to an evaluable reference.")
+
+let intern_evaluable ist = function
+  | {v=AN qid} ->
+    begin match intern_global_reference ist qid with
+    | ArgVar _ as v -> v
+    | ArgArg (loc, r) ->
+      let short = short_name qid in
+      evalref_of_globref ?loc ?short r
+    end
   | {v=ByNotation (ntn,sc);loc} ->
-      evaluable_of_global_reference ist.genv
-      (Notation.interp_notation_as_global_reference ?loc
-        GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
+    let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in
+    let r = Notation.interp_notation_as_global_reference ?loc check ntn sc in
+    evalref_of_globref ?loc r
 
 let intern_smart_global ist = function
   | {v=AN r} -> intern_global_reference ist r
@@ -318,21 +324,6 @@ let intern_smart_global ist = function
       ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc
         GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
 
-(* Globalize a reduction expression *)
-let intern_evaluable ist r =
-  let f ist r =
-    let e = intern_evaluable_reference_or_by_notation ist r in
-    let na = short_name r in
-    ArgArg (e,na)
-  in
-  match r with
-  | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist ->
-    ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
-  | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist ->
-    let id = qualid_basename qid in
-      ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id))
-  | _ -> f ist r
-
 let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
 
 let intern_flag ist red =
@@ -393,10 +384,10 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
       let c = Constrintern.interp_reference sign r in
       match DAst.get c with
       | GRef (r,None) ->
-          Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
+          Inl (evalref_of_globref r)
       | GVar id ->
-          let r = evaluable_of_global_reference ist.genv (GlobRef.VarRef id) in
-          Inl (ArgArg (r,None))
+          let r = evalref_of_globref (GlobRef.VarRef id) in
+          Inl r
       | _ ->
           let bound_names = Glob_ops.bound_glob_vars c in
           Inr (bound_names,(c,None),dummy_pat) in
diff --git a/test-suite/bugs/closed/bug_4925.v b/test-suite/bugs/closed/bug_4925.v
new file mode 100644
index 0000000000..d4e4b35351
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4925.v
@@ -0,0 +1,6 @@
+Axiom a: bool.
+
+Goal a = true.
+Proof.
+try unfold a.
+Abort.
diff --git a/test-suite/bugs/closed/bug_5159.v b/test-suite/bugs/closed/bug_5159.v
new file mode 100644
index 0000000000..cbc924c2d3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5159.v
@@ -0,0 +1,12 @@
+Axiom foo : Type.
+Definition bar := 1.
+Definition bar' := Eval cbv -[bar] in bar.
+Declare Reduction red' := cbv -[bar].
+Opaque bar.
+Definition bar'' := Eval red' in bar.
+Declare Reduction red'' := cbv -[bar]. (* Error: Cannot coerce bar to an
+evaluable reference. *)
+Definition bar''' := Eval cbv -[bar] in bar. (* Error: Cannot coerce bar to an
+evaluable reference. *)
+Definition foo' := Eval cbv -[foo] in foo. (* Error: Cannot coerce foo to an
+evaluable reference. *)
diff --git a/test-suite/bugs/closed/bug_5764.v b/test-suite/bugs/closed/bug_5764.v
new file mode 100644
index 0000000000..0b015d9c7e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5764.v
@@ -0,0 +1,7 @@
+Module Type A.
+Parameter a : nat.
+End A.
+
+Module B (mA : A).
+Ltac cbv_a := cbv [mA.a].
+End B.
diff --git a/test-suite/success/with_strategy.v b/test-suite/success/with_strategy.v
index 077b57c87f..6f0833211e 100644
--- a/test-suite/success/with_strategy.v
+++ b/test-suite/success/with_strategy.v
@@ -195,8 +195,8 @@ Opaque F.id.
 
 Goal F.id 0 = F.id 0.
   Fail unfold F.id.
-  (* This should work, but it fails with "Cannot coerce F.id to an evaluable reference." *)
-  Fail F.with_transparent_id ltac:(progress unfold F.id).
+  F.with_transparent_id ltac:(progress unfold F.id).
+  Undo.
   F.with_transparent_id ltac:(let x := constr:(@F.id) in progress unfold x).
 Abort.
 
@@ -212,8 +212,8 @@ Opaque F2.id.
 
 Goal F2.id 0 = F2.id 0.
   Fail unfold F2.id.
-  (* This should work, but it fails with "Cannot coerce F2.id to an evaluable reference." *)
-  Fail F2.with_transparent_id ltac:(progress unfold F2.id).
+  F2.with_transparent_id ltac:(progress unfold F2.id).
+  Undo.
   F2.with_transparent_id ltac:(let x := constr:(@F2.id) in progress unfold x).
 Abort.
 
diff --git a/theories/Floats/FloatLemmas.v b/theories/Floats/FloatLemmas.v
index 29b1451822..1be6d2502a 100644
--- a/theories/Floats/FloatLemmas.v
+++ b/theories/Floats/FloatLemmas.v
@@ -49,7 +49,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
   rewrite Hmod_elim.
   clear Hmod_elim.
   revert Hv.
-  unfold valid_binary, bounded, canonical_mantissa.
+  unfold SpecFloat.valid_binary, bounded, canonical_mantissa.
   unfold fexp.
   rewrite Bool.andb_true_iff.
   intro H'.
@@ -62,7 +62,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
     destruct (Z.max_spec (Z.pos (digits2_pos m) + e0 - prec) emin) as [ (H, Hm) | (H, Hm) ].
     + rewrite Hm in H1.
       rewrite <- H1.
-      rewrite !Z.max_l by (revert He; unfold emax, emin, prec; lia).
+      rewrite !Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
       replace (emin + _)%Z with emax by ring.
       unfold shl_align.
       rewrite <- H1 in H.
@@ -74,7 +74,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       unfold fexp.
       unfold Zdigits2.
       unfold shr_record_of_loc, shr.
-      rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia).
+      rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
       replace (_ - _)%Z with (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z by ring.
       assert (Hs : (Z.pos (digits2_pos (shift_pos p m)) <= prec)%Z).
       {
@@ -103,26 +103,26 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       unfold round_nearest_even.
       remember (Z.pos (digits2_pos (shift_pos p m)) - prec)%Z as ds.
       destruct ds.
-      * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
+      * rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
         replace (_ - _)%Z with Z0 by lia.
         replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
-        rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
+        rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
         replace (_ - _)%Z with Z0 by lia.
-        rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
+        rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
         replace (_ - _)%Z with Z0 by lia.
         replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
         reflexivity.
       * exfalso; lia.
-      * rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
+      * rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
         replace (_ - _)%Z with (Zneg p0) by lia.
         replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
-        rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
+        rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
         replace (_ - _)%Z with (Zneg p0) by lia.
-        rewrite Z.max_l by (revert He; unfold emax, emin, prec; lia).
+        rewrite Z.max_l by (revert He; unfold emax, SpecFloat.emin, prec; lia).
         replace (_ - _)%Z with (Zneg p0) by lia.
         replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
         reflexivity.
-    + rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia).
+    + rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
       rewrite Hm in H1.
       clear Hm.
       replace (Zpos _ + _ - _)%Z with (e0 + (emax - emin))%Z by (rewrite <- H1 at 1; ring).
@@ -134,7 +134,7 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       unfold shr_fexp.
       unfold fexp.
       unfold Zdigits2.
-      rewrite !Z.max_l by (revert H He; unfold emax, emin, prec; lia).
+      rewrite !Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
       unfold shr_record_of_loc.
       unfold shr.
       unfold Zdigits2.
@@ -142,17 +142,17 @@ Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2S
       unfold shr_m.
       unfold loc_of_shr_record.
       unfold round_nearest_even.
-      rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia).
+      rewrite Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
       replace (Zpos _ + _ - _ - _)%Z with Z0 by lia.
       replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
       replace (Zpos _ + _ - _ - _)%Z with Z0 by lia.
-      rewrite Z.max_l by (revert H He; unfold emax, emin, prec; lia).
+      rewrite Z.max_l by (revert H He; unfold emax, SpecFloat.emin, prec; lia).
       replace (Zpos _ + _ - _ - _)%Z with Z0 by lia.
       replace (_ <=? _)%Z with false by (symmetry; rewrite Z.leb_gt; lia).
       reflexivity.
   - rewrite Z.min_le_iff.
     intro H.
-    destruct H as [ He | Habs ]; [ | revert Habs; now unfold emin, emax ].
+    destruct H as [ He | Habs ]; [ | revert Habs; now unfold SpecFloat.emin, emax ].
     unfold shl_align.
     assert (Hprec : (Z.pos (digits2_pos m) <= prec)%Z).
     {