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
...
*
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
*
- Optimized "auto decomp" which had a (presumably) exponential in
herbelin
2008-12-26
*
FMap: fold_rec + more permissive transpose hyp + various cleanup
letouzey
2008-12-22
*
FSets: integration of suggestions by P. Casteran and S. Lescuyer
letouzey
2008-12-18
*
Better compatibility after commit 11693 by adding an alias OrderedTypeFacts.e...
letouzey
2008-12-17
*
FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...
letouzey
2008-12-17
*
Take advantage of natdynlink when available: almost all contribs become loada...
letouzey
2008-12-16
*
Move FunctionalExtensionality to Logic/ (someone please check that the
msozeau
2008-12-16
*
Finish fix for the treatment of [inverse] in [setoid_rewrite], making a
msozeau
2008-12-16
*
Generalized binding syntax overhaul: only two new binders: `() and `{},
msozeau
2008-12-14
*
Uniformity with the rest of the StdLib : _symm --> _sym
letouzey
2008-12-12
*
Structural definition of PositiveMap.fold
glondu
2008-12-11
*
Make PositiveMap.xmapi structural
glondu
2008-12-11
*
Fix handling of [inverse] in setoid_rewrite, with an hopefully complete
msozeau
2008-12-08
*
Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lasson
msozeau
2008-12-04
*
Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b
herbelin
2008-11-23
*
- Fixed minor bug #1994 in the tactic chapter of the manual [doc]
herbelin
2008-11-22
*
integrate suggestions by B. Baydemir (see #1930)
letouzey
2008-11-17
[prev]
[next]