index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
Commit message (
Expand
)
Author
Age
*
Miscellaneous practical commits:
herbelin
2009-06-29
*
made several occurrences of (eapply ...; eauto) not rely on the lack of patte...
barras
2009-06-22
*
Do a fixpoint on the result of typeclass search to force the
msozeau
2009-06-08
*
- Added two new introduction patterns with the following temptative syntaxes:
herbelin
2009-06-07
*
Very-small-step policy changes to the library.
herbelin
2009-06-06
*
Use Type instead of Set.
msozeau
2009-06-02
*
Stop using a "Manual Implicit Arguments" flag and support them as soon
msozeau
2009-05-27
*
Many fixes in unification:
msozeau
2009-05-20
*
Minor fixes in typeclasses:
msozeau
2009-05-16
*
adds a theorem to reason at the level of Z
bertot
2009-05-07
*
Improvements in typeclasses eauto and generalized rewriting:
msozeau
2009-05-05
*
Fixes for bugs in r12110:
msozeau
2009-04-28
*
Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs
herbelin
2009-04-28
*
- Implementation of a new typeclasses eauto procedure based on success
msozeau
2009-04-27
*
Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
herbelin
2009-04-24
*
Rename [Morphism] into [Proper] and [respect] into [proper] to comply
msozeau
2009-04-21
*
Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact that
msozeau
2009-04-20
*
Just export RelationClasses for [Equivalence] through Setoid.
msozeau
2009-04-18
*
Only export the notations of Morphism as well as Equivalence through
msozeau
2009-04-17
*
Better Requires in Classes. Fix bug #2093: the code does not require
msozeau
2009-04-16
*
Rewrite autorewrite to use a dnet indexed by the left-hand sides (or
msozeau
2009-04-14
*
Some additions in Max and Zmax. Unifiying list of statements and names
herbelin
2009-04-14
*
Rewrite of setoid_rewrite to modularize it based on proof-producing
msozeau
2009-04-13
*
Fix premature optimisation in dependent induction: even variable args need
msozeau
2009-04-10
*
Experimental support for automatic destruction of recursive calls and
msozeau
2009-04-08
*
Move setoid_rewrite to its own module and do some clean up in
msozeau
2009-04-07
*
Ocamlbuild: improvements suggested by N. Pouillard
letouzey
2009-04-03
*
Rewrite of Program Fixpoint to overcome the previous limitations:
msozeau
2009-03-28
*
ZArith/Int: no need to load romega here (but rather in FullAVL)
letouzey
2009-03-28
*
Parsing files for numerals (+ ascii/string) moved into plugins
letouzey
2009-03-27
*
fixed ring/field warning about hyp cleaning up
barras
2009-03-18
*
- gros commit sur ring et field: passage des arguments simplifie
barras
2009-03-17
*
Better mechanism for loading initial plugins
letouzey
2009-03-14
*
Cyclic31: proof of a forgotten admit
letouzey
2009-02-10
*
Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]
herbelin
2009-02-06
*
Fix [subrelation] clauses that privileged the weakest. Better impl args
msozeau
2009-02-04
*
Report r11631 from 8.2 and handle non-dependent goals better in
msozeau
2009-02-04
*
FSet(Weak)List : eq_dec becomes Defined (and gets better proof)
letouzey
2009-01-28
*
- Fixed various Overfull in documentation.
herbelin
2009-01-27
*
- Better deal with commands inside section titles in latex output using
msozeau
2009-01-21
*
Various little fixes:
msozeau
2009-01-18
*
Getting rid of the previous implementation of setoid_rewrite which was
msozeau
2009-01-18
*
Last changes in type class syntax:
msozeau
2009-01-18
*
- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",
herbelin
2009-01-02
*
Switched to "standardized" names for the properties of eq and
herbelin
2009-01-01
*
- Fixed bug #2021 (uncaught exception with injection/discriminate when
herbelin
2009-01-01
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
FMaps: various updates (mostly suggested by P. Casteran)
letouzey
2008-12-26
*
- Extracted from the tactic "now" an experimental tactic "easy" for small
herbelin
2008-12-26
[next]