index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
In the short term, stronger invariant on the syntax of TacAssert, what
Hugo Herbelin
2016-04-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-04-09
|
\
|
*
Allow to unset the refinement mode of Instance in ML
Matthieu Sozeau
2016-04-07
|
*
Fixing an incorrect use of prod_appvect on a term which was not a
Hugo Herbelin
2016-04-07
|
*
Fixing the "No applicable tactic" non informative error message
Hugo Herbelin
2016-04-03
*
|
Moving Autorewrite back to tactics/.
Pierre-Marie Pédrot
2016-03-25
*
|
Moving Eqdecide to tactics/.
Pierre-Marie Pédrot
2016-03-25
*
|
Moving Eauto and Class_tactics to tactics/.
Pierre-Marie Pédrot
2016-03-25
*
|
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
*
|
Moving Tacsubst to hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
Relying on generic arguments to represent Extern hints.
Pierre-Marie Pédrot
2016-03-20
*
|
Adding a new Ltac generic argument for forced tactics returing unit.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Tacenv to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Tactic_debug to Hightactic.
Pierre-Marie Pédrot
2016-03-20
*
|
Making Evarutil independent from Reductionops.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Refine to its proper module.
Pierre-Marie Pédrot
2016-03-20
*
|
Making Proofview independent of Logic.
Pierre-Marie Pédrot
2016-03-20
*
|
Fixing the classification of Tactic Notation.
Pierre-Marie Pédrot
2016-03-20
|
*
Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Tacintern to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving the tactic related code from Metasyntax to a new file.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Print Ltac to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Tacinterp to Hightactics.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving the use of Tactic_option from Obligations to G_obligations.
Pierre-Marie Pédrot
2016-03-19
*
|
Removing the special status of generic arguments defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
|
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
*
|
Adding a universe argument to Pcoq.create_generic_entry.
Pierre-Marie Pédrot
2016-03-17
*
|
Removing the registering of default values for generic arguments.
Pierre-Marie Pédrot
2016-03-17
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-09
|
\
|
*
|
Redo fix init_setoid -> init_relation_classes
Matthieu Sozeau
2016-03-09
|
*
Fix strategy of Keyed Unification
Matthieu Sozeau
2016-03-09
*
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
Putting Tactic_debug just below Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
|
Removing dependency of Himsg in tactic files.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Tactic_debug to tactics/ folder.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Ltac traces to Tacexpr and Tacinterp.
Pierre-Marie Pédrot
2016-03-06
*
|
Removing useless grammar.cma dependencies.
Pierre-Marie Pédrot
2016-03-06
*
|
Moving Eauto to a simple ML file.
Pierre-Marie Pédrot
2016-03-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
*
|
Exporting build_selector, a component of discriminate, for use in congruence.
Hugo Herbelin
2016-03-05
*
|
Adding some standard arguments in tactic scopes.
Pierre-Marie Pédrot
2016-03-04
*
|
Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].
Pierre-Marie Pédrot
2016-03-04
*
|
Removing the UConstr entry of the tactic_arg AST.
Pierre-Marie Pédrot
2016-03-04
*
|
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
[next]
Hugo Herbelin
Pierre-Marie Pédrot
Matthieu Sozeau