| Commit message (Collapse) | Author | Age |
| |
|
| |
|
|
|
|
|
|
|
| |
This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0.
I had mixed up the boolean flag, resulting in the loss of evar-free
versions of tactics.
|
| |
|
|
|
|
|
|
| |
there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
|
| |
|
|
|
|
| |
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
|
|
|
|
| |
The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
|
| |
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
Indeed [tclWITHHOLES false tac sigma x] is equivalent to [tclEVARS sigma <*> tac x]
and we should try to reduce the use of this tactical, because it is mostly
a legacy tactic.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
all the tactics using the constructor keyword in one entry. This has the
side-effect to also remove the other variant of constructor from the AST.
I also needed to hack around the "tauto" tactic to make it work, by
calling directly the ML tactic through a TacExtend node. This may be
generalized to get rid of the intermingled dependencies between this
tactic and the infamous Ltac quotation mechanism.
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
variant of it, accepting an additional integer.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
| |
"foobar" constr(x1) ... constr(xn)
are now defined as pure Ltac definitions, and do not add grammar
nor printing rules. This partially relies on a hack consisting
in retrieving the arguments in the tactic environment rather than
as directly passed to the TacExtend node.
|
|
|
|
|
|
|
|
| |
We eta-expand primitive Ltac functions, and instead of feeding TacExtend
directly with its arguments, we use the environment to retrieve them.
Some tactics from the AST were also moved away and made using this
mechanism.
|
|
"coretactics.ml4" file.
|