index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_tactic.ml4
Commit message (
Expand
)
Author
Age
*
Removing useless grammar entries. Fixes bug #4919.
Pierre-Marie Pédrot
2016-07-18
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Add and document match, fix and cofix reduction flags.
Maxime Dénès
2016-07-01
*
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-06-18
*
Adding eintros to respect the e- prefix policy.
Hugo Herbelin
2016-06-18
*
Fixing a mispelling coma -> comma.
Hugo Herbelin
2016-06-16
*
A stronger invariant on the syntax of TacAssert, what allows for a
Hugo Herbelin
2016-06-16
*
Removing "rename" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "exact" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "intro" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "double induction" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
g_tactics : remove opt_bindings (2-line dead code)
Pierre Letouzey
2016-06-01
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
|
*
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-09
*
|
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
Hugo Herbelin
2016-04-27
*
|
Revert "Fixing a mispelling coma -> comma."
Hugo Herbelin
2016-04-27
*
|
Fixing a mispelling coma -> comma.
Hugo Herbelin
2016-04-27
*
|
In the short term, stronger invariant on the syntax of TacAssert, what
Hugo Herbelin
2016-04-27
*
|
Moving the "move" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "exists" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "symmetry" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "generalize dependent" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "clearbody" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "clear" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "cofix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Moving the "fix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
|
Stronger invariants on the use of the introduction pattern (pat1,...,patn).
Hugo Herbelin
2016-01-21
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Removing unused parsing entries.
Pierre-Marie Pédrot
2015-12-28
*
|
Removing the special status of open_constr generic argument.
Pierre-Marie Pédrot
2015-12-28
*
|
Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.ml
Hugo Herbelin
2015-12-25
*
|
Removing auto from the tactic AST.
Pierre-Marie Pédrot
2015-12-24
*
|
Tactics: Generalizing the use of the experimental clearing modifier to
Hugo Herbelin
2015-12-15
|
/
*
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Hugo Herbelin
2015-12-10
*
Changing "destruct !hyp" into "destruct (hyp)" (and similarly for induction)
Hugo Herbelin
2015-12-05
*
Improving syntax of pat/constr introduction pattern so that
Hugo Herbelin
2015-12-02
*
Dead code from August 2014 in apply in.
Hugo Herbelin
2015-12-02
*
Manually expand red_tactic so that notations do not break reduction tactics. ...
Guillaume Melquiond
2015-10-30
*
Manually expand the debugging versions of "trivial" and "auto". (Fix bug #4392)
Guillaume Melquiond
2015-10-29
*
grammar: export hypident
Enrico Tassi
2015-03-30
*
Update headers.
Maxime Dénès
2015-01-12
*
Extend the syntax of simpl with a delta flag.
Arnaud Spiwack
2014-12-12
*
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
*
Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".
Hugo Herbelin
2014-11-02
*
Reorganization of the test for generic selection of occurrences in
Hugo Herbelin
2014-10-31
*
Dead code
Hugo Herbelin
2014-10-27
[next]