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 | |
| parent | d640d9debf449dad1f7b1d2eda44a024b78378d1 (diff) | |
| parent | c43231d47ce1c3904acc3b6f531aa3762791871e (diff) | |
Merge PR #12254: In non-strict mode, accept any variable as a tactic reference.
Reviewed-by: herbelin
| -rw-r--r-- | doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst | 5 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 13 | ||||
| -rw-r--r-- | test-suite/success/tac_wit_ref.v | 8 |
3 files changed, 23 insertions, 3 deletions
diff --git a/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst b/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst new file mode 100644 index 0000000000..69632fd202 --- /dev/null +++ b/doc/changelog/05-tactic-language/12254-wit-ref-dyn.rst @@ -0,0 +1,5 @@ +- **Changed:** + The "reference" tactic generic argument now accepts arbitrary + variables of the goal context + (`#12254 <https://github.com/coq/coq/pull/12254>`_, + by Pierre-Marie Pédrot). 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 diff --git a/test-suite/success/tac_wit_ref.v b/test-suite/success/tac_wit_ref.v new file mode 100644 index 0000000000..8bde31858e --- /dev/null +++ b/test-suite/success/tac_wit_ref.v @@ -0,0 +1,8 @@ +Tactic Notation "foo" reference(n) := idtac n. + +Goal forall n : nat, n = 0. +Proof. +intros n. +foo nat. +foo n. +Abort. |