diff options
| author | Hugo Herbelin | 2020-05-11 22:18:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-11 22:18:42 +0200 |
| commit | 00328b2165b68c81eef0a6bf1c5483f8e906a31d (patch) | |
| tree | 1842b07d42094c15f91ef2f3bd02e7f507a8d80b /plugins | |
| parent | d640d9debf449dad1f7b1d2eda44a024b78378d1 (diff) | |
| parent | c43231d47ce1c3904acc3b6f531aa3762791871e (diff) | |
Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.
Reviewed-by: herbelin
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 929fd5e132..1aa3af0087 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 |