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
...
*
New version of 12650 that was broken (supporting again records when
herbelin
2010-01-12
*
Added module sharing support for typeclasses and hints (pri_auto_tactic).
soubiran
2010-01-12
*
revert commit 12650 for the moment, since it breaks MSetAVL
letouzey
2010-01-12
*
Temporary fix to compensate the loss of descent on dependent
herbelin
2010-01-12
*
Fixing bug #2146 (broken selection of occurrences in "change").
herbelin
2009-12-30
*
Improving descend_in_conjunctions (using a combinators instead of a tactic)
herbelin
2009-12-29
*
Safer, though ad hoc, approach to re-interpretation of the argument of
herbelin
2009-12-28
*
Fix "Existing Instance" to handle globality information and "Existing
msozeau
2009-12-27
*
In "simpl c" and "change c with d", c can be a pattern.
herbelin
2009-12-24
*
Opened the possibility to type Ltac patterns but it is not fully functional yet
herbelin
2009-12-24
*
Moved a bit further the code for pattern interpretation in match goal
herbelin
2009-12-23
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Backtrack on making exact hints for lemmas starting with products
msozeau
2009-12-19
*
adding an option functional_induction_rewrite_dependent to make functional in...
jforest
2009-12-16
*
Improved strategy for rewriting lemma possibly depending because of evars.
herbelin
2009-12-14
*
Made the side-conditions of lemmas always come last when chaining "apply in"
herbelin
2009-12-13
*
Completion of r12580 (better rendering of dependent rewrite and inversion).
herbelin
2009-12-13
*
Revision 12557 continued (better rendering of dependent rewrite)
herbelin
2009-12-13
*
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-12-12
*
Improved the rendering of "dependent rewrite" and hence of "inversion"
herbelin
2009-12-12
*
Turn evars created by a tactic application into a subgoal immediately in
msozeau
2009-12-06
*
Fix anomaly when using typeclass resolution with filtered hyps in evars.
msozeau
2009-12-06
*
Restored rewriting of JMeq using JMeq_rect and co when the domains are the same
herbelin
2009-12-03
*
Fix make_exact_entry to allow applying [forall x, P x] hints directly,
msozeau
2009-12-01
*
Fix bug in typeclass resolution. Better handling of universes in
msozeau
2009-12-01
*
Fix backtracking heuristic in typeclass resolution.
msozeau
2009-11-30
*
Substitute terms for evars-as-goals as soon as they are solved in
msozeau
2009-11-27
*
Minor fixes in typeclasses, avoiding repeated evar normalizations.
msozeau
2009-11-24
*
Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...
puech
2009-11-21
*
Addendum to revision 12501.
herbelin
2009-11-12
*
Promote evar_defs to evar_map (in Evd)
glondu
2009-11-11
*
Backtracking on the use of automatically generated schemes for
herbelin
2009-11-11
*
Compatibility ocaml <= 3.09
herbelin
2009-11-10
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Quick fix for restoring a left-to-right rewriting lemma compatible
herbelin
2009-11-09
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
- Fix discharge bug in typeclasses: some constrs were not actually
msozeau
2009-11-06
*
Misc fixes.
msozeau
2009-11-06
*
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-11-04
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Clarification in comments
glondu
2009-10-28
*
Remove old compatibility stuff (Tacred.nf)
glondu
2009-10-28
*
Make usage of Dyn explicit
glondu
2009-10-28
*
Backport fix for indexing of sorts which collapse every Type occurrence
msozeau
2009-10-28
*
Fixes around typeclasses:
msozeau
2009-10-27
*
fix previous commit
corbinea
2009-10-27
*
fixed czar bug with parametric inductives
corbinea
2009-10-27
*
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
*
Restore (and test) broken chaining of lemmas in "apply in" in presence
herbelin
2009-10-25
*
Add support for remaining side-conditions in "apply in as".
herbelin
2009-10-25
[prev]
[next]