From be56f39ecfc0726772cc6930dbc7657348f008e1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 May 2020 14:19:04 +0200
Subject: 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.
---
 plugins/ltac/tacintern.ml | 59 ++++++++++++++++++++---------------------------
 1 file changed, 25 insertions(+), 34 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3


From 3af3409a8ec23deb3e0d32f00a31363a36f6209b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 8 May 2020 16:29:30 +0200
Subject: Generalize the interpretation of syntactic notation as reference to
 their head.

This seems to be a pattern used quite a bit in the wild, it does not hurt
to be a bit more lenient to tolerate this kind of use. Interestingly the
API was already offering a similar generalization in some unrelated places.

We also backtrack on the change in Floats.FloatLemmas since it is an instance
of this phenomenon.
---
 plugins/ltac/tacintern.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index ff1e8b92d1..fcedbe8e2e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -97,7 +97,7 @@ let intern_global_reference ist qid =
   else if qualid_is_ident qid && find_hyp (qualid_basename qid) ist then
     let id = qualid_basename qid in
     ArgArg (qid.CAst.loc, GlobRef.VarRef id)
-  else match locate_global_with_alias qid with
+  else match locate_global_with_alias ~head:true qid with
   | r -> ArgArg (qid.CAst.loc, r)
   | exception Not_found ->
     if not !strict_check && qualid_is_ident qid then
@@ -315,13 +315,13 @@ let intern_evaluable ist = function
     end
   | {v=ByNotation (ntn,sc);loc} ->
     let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in
-    let r = Notation.interp_notation_as_global_reference ?loc check ntn sc in
+    let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in
     evalref_of_globref ?loc r
 
 let intern_smart_global ist = function
   | {v=AN r} -> intern_global_reference ist r
   | {v=ByNotation (ntn,sc);loc} ->
-      ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc
+      ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc ~head:true
         GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
 
 let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
-- 
cgit v1.2.3


From 5e1da5b05860750606f32063a221d6023cabf5dc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 9 May 2020 15:56:55 +0200
Subject: Tweak the error message of reference internalization.

---
 plugins/ltac/tacintern.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index fcedbe8e2e..53dc518bd3 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -302,8 +302,14 @@ 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 tpe = match r with
+    | GlobRef.IndRef _ -> "inductive"
+    | GlobRef.ConstructRef _ -> "constructor"
+    | (GlobRef.VarRef _ | GlobRef.ConstRef _) -> assert false
+    in
+    user_err ?loc (str "Cannot turn" ++ spc () ++ str tpe ++ spc () ++
+      Nametab.pr_global_env Id.Set.empty r ++ spc () ++
+      str "into an evaluable reference.")
 
 let intern_evaluable ist = function
   | {v=AN qid} ->
-- 
cgit v1.2.3