| Commit message (Expand) | Author | Age |
|---|
| * | Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of... |  letouzey | 2007-11-06 |
| * | useless Require Export Extraction | letouzey | 2007-11-06 |
| * | For debugging with coqtop.byte with ocaml 3.10, the toplevel should be made w... | letouzey | 2007-11-05 |
| * | Suppress from the ouputs of SearchAbout all lemmas generated by "abstract" | letouzey | 2007-11-05 |
| * | Fix bug#1739 |  msozeau | 2007-11-04 |
| * | An update of theories/Numbers |  emakarov | 2007-11-03 |
| * | two additionnal results on list append (coming from theories/ints/List/ListAu... | letouzey | 2007-11-01 |
| * | A way to specialize universally quantified hypothesis: if H is | letouzey | 2007-11-01 |
| * | Adding Qround.v (and helper lemmas and hints) |  roconnor | 2007-11-01 |
| * | In agreement with Laurent Thery, start migration of auxiliary results | letouzey | 2007-11-01 |
| * | temporary workaround for bug #1738 | letouzey | 2007-10-30 |
| * | A useless Add Morphism: since Subset is a Setoid Relation, it is also | letouzey | 2007-10-30 |
| * | bug in safe_typing: univ constraints generated by section variables were not ... |  barras | 2007-10-30 |
| * | Changement esthétique de la preuve de mult_is_one |  notin | 2007-10-30 |
| * | Ajout de lemmes d'inversion pour mult (sur le modèle de plus_is_O et plus_is... | notin | 2007-10-30 |
| * | Cleaning code and comment. |  courtieu | 2007-10-30 |
| * | Revision of the FSetWeak Interface, so that it becomes a precise | letouzey | 2007-10-29 |
| * | Amélioration du message d'erreur dans end_module, end_module_type et close_s... | notin | 2007-10-29 |
| * | MAJ |  herbelin | 2007-10-29 |
| * | Réparation d'une inefficacité bêtement introduite dans la révision | herbelin | 2007-10-27 |
| * | small fix of commit 10188: a string given via Extract Inductive can be empty | letouzey | 2007-10-25 |
| * | Adding BigQ and proofs |  thery | 2007-10-25 |
| * | Added NIso.v to Makefile.common. Changed Examples.v in contrib/micromega to u... | emakarov | 2007-10-25 |
| * | Quelques exemples à méditer sur le polymorphisme d'universe des inductifs | herbelin | 2007-10-24 |
| * | Fix define body bug fix | msozeau | 2007-10-24 |
| * | Fix define body bug | msozeau | 2007-10-24 |
| * | Addition of more general tactics for equality. Functional extensionality and ... | msozeau | 2007-10-24 |
| * | Bugfix in abstract_generalize | msozeau | 2007-10-24 |
| * | Doc update | msozeau | 2007-10-24 |
| * | Fix some bugs, add possibility of automatically solving a proof statement's o... | msozeau | 2007-10-24 |
| * | Enlevé les trucs commités au mauvais endroit |  aspiwack | 2007-10-23 |
| * | Quelques structures de donnée plus les modules principaux (et | aspiwack | 2007-10-23 |
| * | Added "is_empty" to gmap. | aspiwack | 2007-10-23 |
| * | Ajout de mots clés pour Coqdoc (bug #1732) | notin | 2007-10-23 |
| * | Added Numbers/Natural/Abstract/NIso.v that proves that any two models of natu... | emakarov | 2007-10-23 |
| * | Corrections des bugs #1730 et #1731 | notin | 2007-10-22 |
| * | An error message instead of an empty extraction when the monolithic | letouzey | 2007-10-21 |
| * | Avoid the auto-inlining of small fixpoints like List.map. | letouzey | 2007-10-21 |
| * | Cleanup attempt of Hints in *Interface.v files. | letouzey | 2007-10-21 |
| * | Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le | roconnor | 2007-10-19 |
| * | Intallation des .cma/.cmxa | notin | 2007-10-18 |
| * | Changed RingMicromega to use NRing instead of Ring_polynom. NRing is a versio... | emakarov | 2007-10-18 |
| * | Copie de PreOmega.vo dans le répertoire d'installation de Coq | notin | 2007-10-18 |
| * | Copie des .cma et des .cmxa, et de grammar.cma dans le répertoire de Coq (po... | notin | 2007-10-18 |
| * | Typo dans Makefile.common | notin | 2007-10-18 |
| * | Report de la révision #10197 (adaptation à Lablgtk 2.10.0) | notin | 2007-10-18 |
| * | Uniformisation de l'option -where de coqc avec celle de coqtop | notin | 2007-10-18 |
| * | added generation from trivial patterns for congruence |  corbinea | 2007-10-18 |
| * | Repair Haskell/Scheme extraction in the new extraction backend design: | letouzey | 2007-10-17 |
| * | Major reorganisation of the extraction "backend". | letouzey | 2007-10-17 |
letouzey
msozeau
emakarov
roconnor
barras
notin
courtieu
herbelin
thery
aspiwack
corbinea