diff options
| author | Pierre-Marie Pédrot | 2020-05-05 13:57:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-08 16:10:20 +0200 |
| commit | c43231d47ce1c3904acc3b6f531aa3762791871e (patch) | |
| tree | 8649c4a3c0e8a4519615ee22d497a589098ae9fd /plugins | |
| parent | e4bfbdfc4b4944d6e6d702eb732bce24f962e67f (diff) | |
In non-strict mode, accept any variable as a tactic reference.
Part of the plan of #11840.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 13 |
1 files changed, 10 insertions, 3 deletions
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 |