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 | |
| parent | e4bfbdfc4b4944d6e6d702eb732bce24f962e67f (diff) | |
In non-strict mode, accept any variable as a tactic reference.
Part of the plan of #11840.
| -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 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 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. |