Merge PR #12256: Move the static check of evaluability in unfold tactic to runtime.

Reviewed-by: herbelin

1 files changed, 33 insertions, 36 deletions

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 1aa3af0087..53dc518bd3 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
@@ -98,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
@@ -294,45 +293,43 @@ 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 ->
+    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} ->
+    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 ~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))
 
-(* 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 +390,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