index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
extratactics.ml4
Commit message (
Expand
)
Author
Age
*
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-17
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
A new tactic is_var to check whether a term is a goal/section variable
letouzey
2011-10-07
*
Moving implicit tactic support from Tacinterp to Pfedit and final evar
herbelin
2011-09-26
*
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
Rename the "raw" argument extension into "glob"
glondu
2010-12-27
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Add tactic has_evar (#2433)
glondu
2010-12-02
*
Add tactic is_evar (Closes: #2433)
glondu
2010-12-02
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
glondu
2010-09-30
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Adding the destauto tactic, that reduces match by destructing matched
courtieu
2010-07-22
*
Finish adding out-of-the-box support for camlp4
letouzey
2010-07-09
*
Made "replace" accepts open terms on its left-hand-side.
herbelin
2010-06-28
*
Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Update CHANGES, add documentation for new commands/tactics and do a bit
msozeau
2010-01-30
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-12-12
*
Minor fixes in typeclasses, avoiding repeated evar normalizations.
msozeau
2009-11-24
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Move out JMeq of subst for compatibility (it affects e.g. the
herbelin
2009-08-06
*
Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"
letouzey
2009-07-24
*
Add new variants of [rewrite] and [autorewrite] which differ in the
msozeau
2009-06-30
*
- Fixing declarative mode in presence of high use of Change_evars nodes
herbelin
2009-05-20
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
Rewrite autorewrite to use a dnet indexed by the left-hand sides (or
msozeau
2009-04-14
*
Getting rid of the previous implementation of setoid_rewrite which was
msozeau
2009-01-18
*
Finish fix for the treatment of [inverse] in [setoid_rewrite], making a
msozeau
2008-12-16
*
About "apply in":
herbelin
2008-12-09
*
Port [rewrite] tactics to open terms. Currently no check that evars
msozeau
2008-11-05
*
Fixes and refinements regarding occurrence selection:
herbelin
2008-10-26
*
Various little improvements:
msozeau
2008-09-25
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Fixes in generalize_eqs/dependent induction to allow the user to specify
msozeau
2008-07-28
*
New tactics [conv] to test convertibility (actually, unification) of two
msozeau
2008-07-22
*
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-21
*
Correction du bug des types singletons pas sous-type de Set
herbelin
2008-04-27
*
Plug the new setoid implemtation in, leaving the original one commented
msozeau
2008-03-06
[next]