| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
ML tactics that may be used as simple identifiers are now declared as
a true Ltac entry pertaining to the module that contains the Declare ML
Module statement.
|
|
|
|
|
| |
This allows to directly register globtactics in the Tacenv API, without
having to resort to any internalization function.
|
|
|
|
|
| |
Also taking advantage of the change to rename it into TacML. Ultimately
should allow ML tactic to return values.
|
|
|
|
| |
potentially conflicting tactics names from different plugins.
|
| |
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17080 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Instead of putting the body directly in the AST, we register it in a table.
This time it should work properly. Tactic notation are given kernel names to
ensure the unicity of their contents.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17079 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Tactics notation interpretation was messed up because of the use of
identical keys for different notations. All my tentative fixes were
unsuccessful, so better blankly revert the commit for now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Instead of putting the body directly in the AST, we register it in a table.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17077 85f007b7-540e-0410-9357-904b9bb8a0f7
|