| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Removed 'Toplevel' language from extraction documentation, since it is not cu... |  gmelquio | 2009-11-04 |
| * | 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-03 |
| * | 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-11-02 |
| * | 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-30 |
| * | 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-29 |
| * | 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-28 |
| * | 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-27 |
| * | 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-26 |
| * | Restore (and test) broken chaining of lemmas in "apply in" in presence | herbelin | 2009-10-25 |
| * | fixed bug in Czar grammar | corbinea | 2009-10-25 |
gmelquio
notin
herbelin
letouzey
puech
glondu
msozeau
soubiran
corbinea