| Age | Commit message (Expand) | Author |
|---|
| 2007-10-30 | 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-29 | 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-27 | Réparation d'une inefficacité bêtement introduite dans la révision | herbelin |
| 2007-10-25 | 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-24 | 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-23 | 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-22 | Corrections des bugs #1730 et #1731 | notin |
| 2007-10-21 | 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-19 | Adding Zdiv_mod_unique, Zdiv_opp_opp, Zdiv_mult_cancel, and Z_div_le | roconnor |
| 2007-10-18 | 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-17 | Repair Haskell/Scheme extraction in the new extraction backend design: | letouzey |
| 2007-10-17 | Major reorganisation of the extraction "backend". | letouzey |
| 2007-10-17 | Prise en compte des .glob par coq_makefile | notin |
| 2007-10-16 | add visibility of extraction messages in coqide | letouzey |
| 2007-10-16 | Correction d'un bug de l'appel à make via Coqide | notin |
| 2007-10-16 | Fixed congruence instance generator + changed default depth to 1000 | corbinea |
| 2007-10-16 | Added transitivity and irreflexivity of <, as well as < -elimination for bina... | emakarov |
| 2007-10-16 | Added the doc for the new Scheme Equality command | vsiles |
| 2007-10-16 | Vérification que "rewrite in" se comporte comme "rewrite" et échoue | herbelin |
| 2007-10-15 | build system: When using GOTO_STAGE, always go into that stage, even when tar... | lmamane |
| 2007-10-12 | - Préservation des appels récursifs de tête dans ltac (réponse au "wish" | herbelin |
| 2007-10-12 | Uniformisation du comportement de rewrite et rewrite in : quand le | herbelin |
