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
...
*
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
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
Fixing XML doc (COQ_XML not working as an environment variable).
herbelin
2009-10-24
*
First debug... the renaming of librairies was not working and auto/dn were no...
soubiran
2009-10-23
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Fix bug in typeclass resolution discoverd by Eeelis van der Weegen:
msozeau
2009-10-15
*
Relaxed error severity when encountering unknown library objects or tactic
gmelquio
2009-10-06
*
Correctly do backtracking during type class resolution even if only new
msozeau
2009-10-05
*
Changed the way to support compatibility with previous versions.
herbelin
2009-10-04
*
Removal of trailing spaces.
serpyc
2009-10-04
*
Added option "Unset Dependent Propositions Elimination" to protect
herbelin
2009-10-03
*
Remove legacy export_* functions
glondu
2009-09-29
*
Apply "Declare Implicit Tactic" also to terms interpreted as "open
herbelin
2009-09-27
*
Fixed a bug in the interaction between dEqThen and inject_at_positions
herbelin
2009-09-27
[prev]
[next]