| Age | Commit message (Expand) | Author |
|---|
| 2009-11-04 | Removed 'Toplevel' language from extraction documentation, since it is not cu... | gmelquio |
| 2009-11-03 | Report de la révision #12208 de la v8.2 (correction du bug #2126) | notin |
| 2009-11-03 | Removed debugging stuff mistakenly introduced in r12426. | herbelin |
| 2009-11-03 | Numbers: start using Classes stuff, Equivalence, Proper, Instance, etc | letouzey |
| 2009-11-03 | ROrderedType + Rminmax : Coq's Reals can be seen as OrderedType. | letouzey |
| 2009-11-03 | Better visibility of the inductive CompSpec used to specify comparison functions | letouzey |
| 2009-11-03 | OrderedType implementation for various numerical datatypes + min/max structures | letouzey |
| 2009-11-02 | Reverted an incorrect code simplification in function status_changed | herbelin |
| 2009-11-02 | List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F... | letouzey |
| 2009-11-02 | Remove various useless {struct} annotations | letouzey |
| 2009-11-02 | Added alternate versions of existing lemmas on sqrt. | gmelquio |
| 2009-11-02 | Correction du bug #2175 | notin |
| 2009-11-02 | Sorting/Permutation: no need to require the whole Arith (and hence plugins li... | letouzey |
| 2009-11-02 | Operators_Properties: avoid to depend on Setoid | letouzey |
| 2009-11-02 | list, length, app are migrated from List to Datatypes | letouzey |
| 2009-10-30 | Undo 12432 which caused an exponential behavior at Requires. Compilation time... | puech |
| 2009-10-30 | Attempt to capture on time unification errors for "with" bindings. | herbelin |
| 2009-10-30 | Take constraints into account in the "instantiate" tactic | herbelin |
| 2009-10-30 | Added Coqide highlighting for extraction vernacular. | gmelquio |
| 2009-10-30 | Removed 'dest' from keyword highlighting. | gmelquio |
| 2009-10-29 | Hopefully improved layout of fix guardness error message. | herbelin |
| 2009-10-29 | Fix flat_map definition so that it plays nicely with fix | glondu |
| 2009-10-29 | Fixed some typos in the reference manual. | gmelquio |
| 2009-10-29 | Revision 12439 continued, printing part (notations to names behave | herbelin |
| 2009-10-29 | Fix bug in dnet.ml, which missed some results when filtering one term against... | puech |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-10-28 | Made that notations to names behave like the names they refer to wrt | herbelin |
| 2009-10-28 | Fixed a bug when reporting unexisting reference to an inductive | herbelin |
| 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 | Typo in the refman | puech |
| 2009-10-28 | Fix incorrect registration of objects in libtypes.ml when defining a module. | puech |
| 2009-10-28 | Same as commit 12430 but with the good version of the function iter_all_segment | soubiran |
| 2009-10-28 | From now SearchAbout requests search also inside INCLUDE libobject. | soubiran |
| 2009-10-28 | Module type expressions of the form (Fsig X) with Definition foo := bar are n... | soubiran |
| 2009-10-27 | Add a new vernacular command for controling implicit generalization of | msozeau |
| 2009-10-27 | Fixes around typeclasses: | msozeau |
| 2009-10-27 | Added option --external to coqdoc to bind an url to an external library. | herbelin |
| 2009-10-27 | Documentation of the Local and Global modifiers. | herbelin |
| 2009-10-27 | fix previous commit | corbinea |
| 2009-10-27 | fixed czar bug with parametric inductives | corbinea |
| 2009-10-26 | Fix Setoid documentation. | msozeau |
| 2009-10-26 | Local/Global revision 12418 continued | herbelin |
| 2009-10-26 | Adapted test unfold.v after eq gets its argument maximally inserted | herbelin |
| 2009-10-26 | New cleaning phase of the Local/Global option management | herbelin |
| 2009-10-26 | New functors for gmap and gset. | soubiran |
| 2009-10-25 | Restore (and test) broken chaining of lemmas in "apply in" in presence | herbelin |
| 2009-10-25 | fixed bug in Czar grammar | corbinea |
