index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tacintern.ml
Commit message (
Expand
)
Author
Age
*
Add Ltac syntax for the [tclIFCATCH] primitive.
Arnaud Spiwack
2014-12-12
*
Extend the syntax of simpl with a delta flag.
Arnaud Spiwack
2014-12-12
*
One more word about "simpl f": avoid "simpl f" to be printed "simpl f",
Hugo Herbelin
2014-11-23
*
Hopefully the last word on having "simpl f" complying with the
Hugo Herbelin
2014-11-18
*
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-16
*
Removing a unused boolean in the TacMove node of tacexpr AST.
Pierre-Marie Pédrot
2014-11-09
*
Fixing #3562 ("as" in "destruct" expects either a disjunctive
Hugo Herbelin
2014-11-07
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-07
*
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-30
*
Using an or_var rather than the hack with loc for coding a pure ident
Hugo Herbelin
2014-09-24
*
Removing the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Silence an ocaml warning.
Arnaud Spiwack
2014-09-05
*
Useless hooks in Tacintern.
Pierre-Marie Pédrot
2014-09-03
*
Code factorization in Tacintern.
Pierre-Marie Pédrot
2014-09-03
*
Removing [revert] tactic from the AST.
Pierre-Marie Pédrot
2014-09-02
*
Moving the decompose tactic out of the AST.
Pierre-Marie Pédrot
2014-09-01
*
Code cleaning in Tacintern.
Pierre-Marie Pédrot
2014-09-01
*
Getting rid of atomic tactics in Tacenv.
Pierre-Marie Pédrot
2014-08-31
*
Type-safe version of genarg list / pair / opt functions.
Pierre-Marie Pédrot
2014-08-29
*
Adding a new intro-pattern for "apply in" on the fly. Using syntax
Hugo Herbelin
2014-08-18
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Moving the TacAlias node out of atomic tactics.
Pierre-Marie Pédrot
2014-08-18
*
Moving the TacExtend node from atomic to plain tactics.
Pierre-Marie Pédrot
2014-08-18
*
Removing simple induction / destruct from the AST.
Pierre-Marie Pédrot
2014-08-07
*
Instead of relying on a trick to make the constructor tactic parse, put
Pierre-Marie Pédrot
2014-08-07
*
Removing the "constructor" tactic from the AST.
Pierre-Marie Pédrot
2014-08-07
*
Revert the change in Constrintern introduced by "Add a type of untyped term t...
Arnaud Spiwack
2014-08-06
*
Removing "intros untils" from the AST.
Pierre-Marie Pédrot
2014-08-06
*
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-08-05
*
Adding a syntax "enough" for the variant of "assert" with the order of
Hugo Herbelin
2014-08-05
*
Better struture for Ltac internalization environments in Constrintern.
Pierre-Marie Pédrot
2014-08-02
*
New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.
Arnaud Spiwack
2014-08-01
*
Add [numgoal] to Ltac.
Arnaud Spiwack
2014-08-01
*
Untyped terms in tactic: function [type_term c] to give a typed version of [c].
Arnaud Spiwack
2014-07-29
*
Add a type of untyped term to Ltac's value.
Arnaud Spiwack
2014-07-29
*
Removing dead code relative to or_metaid.
Pierre-Marie Pédrot
2014-07-25
*
Distinguish tactics t1;t2 and t1;[t2..].
Arnaud Spiwack
2014-07-24
*
Adding a "time" tactical for benchmarking purposes. In case the tactic
Hugo Herbelin
2014-07-13
*
Revert "time tac" (committed by mistake).
Hugo Herbelin
2014-07-07
*
time tac
Hugo Herbelin
2014-07-07
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Moving the [split] tactic out of the AST.
Pierre-Marie Pédrot
2014-06-06
*
Moving the "specialize" tactic out of the AST. Also removed an obsolete
Pierre-Marie Pédrot
2014-05-22
*
Removing useless use of metaids in tactic AST.
Pierre-Marie Pédrot
2014-05-22
*
Removing decompose record / sum from the tactic AST.
Pierre-Marie Pédrot
2014-05-21
*
Moving left & right tactics out of the AST.
Pierre-Marie Pédrot
2014-05-21
*
Moving (e)transitivity out of the AST.
Pierre-Marie Pédrot
2014-05-20
*
Tentative to add constr-using primitive tactics without grammar rules.
Pierre-Marie Pédrot
2014-05-20
*
Moving argument-free tactics out of the AST into a dedicated
Pierre-Marie Pédrot
2014-05-16
[next]