From c43231d47ce1c3904acc3b6f531aa3762791871e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 May 2020 13:57:31 +0200
Subject: In non-strict mode, accept any variable as a tactic reference.

Part of the plan of #11840.
---
 plugins/ltac/tacintern.ml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 597c3fdaac..23b590b964 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -95,9 +95,16 @@ let intern_string_or_var = intern_or_var (fun (s : string) -> s)
 let intern_global_reference ist qid =
   if qualid_is_ident qid && find_var (qualid_basename qid) ist then
     ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid)
-  else
-    try ArgArg (qid.CAst.loc,locate_global_with_alias qid)
-    with Not_found -> Nametab.error_global_not_found 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
+  | r -> ArgArg (qid.CAst.loc, r)
+  | exception Not_found ->
+    if not !strict_check && qualid_is_ident qid then
+      let id = qualid_basename qid in
+      ArgArg (qid.CAst.loc, GlobRef.VarRef id)
+    else Nametab.error_global_not_found qid
 
 let intern_ltac_variable ist qid =
   if qualid_is_ident qid && find_var (qualid_basename qid) ist then
-- 
cgit v1.2.3