| Age | Commit message (Expand) | Author |
|---|
| 2008-04-03 | Chgts mineurs: | herbelin |
| 2008-04-03 | Patch sur le typage d'un foncteur applique a un alias. | soubiran |
| 2008-04-02 | Minor fixes. Use expanded type in class_tactics for Morphism search, to | msozeau |
| 2008-04-02 | Add the ability to specify the implicit status of section variables and | msozeau |
| 2008-04-01 | Typo affichage "simple apply" | herbelin |
| 2008-04-01 | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin |
| 2008-04-01 | Ajout "simple apply" et "simple eapply" pour apply sans unfold | herbelin |
| 2008-04-01 | Finish enhancemenent of return clause inference from tycons, integrating | msozeau |
| 2008-04-01 | Enhance handling of parameters in typeclass constraints: permit to specify an... | msozeau |
| 2008-04-01 | Add option to set the opacity of obligations to transparent, to be able | msozeau |
| 2008-04-01 | Correction du bug #1819 | notin |
| 2008-03-31 | - Fix for rewriting under dependent products. | msozeau |
| 2008-03-30 | Suite commit 10730: MAJ xlate.ml | herbelin |
| 2008-03-30 | Modifications diverses et variées : | herbelin |
| 2008-03-30 | Ajout d'abbréviations/notations paramétriques | herbelin |
| 2008-03-29 | Fix test-suite files, change conflicting notation "->rel" and the others | msozeau |
| 2008-03-28 | Improve error handling and messages for typeclasses. | msozeau |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-03-28 | Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression | notin |
| 2008-03-27 | - notations &&& and ||| equivalent to andb and orb, | letouzey |
| 2008-03-27 | Various fixes on typeclasses: | msozeau |
| 2008-03-26 | Diverses petites modifs dans la test-suite: | notin |
| 2008-03-26 | Bug dans la gestion des dépendances vers les .ml | notin |
| 2008-03-26 | Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et coq_m... | notin |
| 2008-03-26 | Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de... | soubiran |
| 2008-03-25 | Prise en compte des dépendances des .ml | notin |
| 2008-03-25 | Correction de bugs relatifs a la compostion des substitutions | soubiran |
| 2008-03-25 | Correction d'un bug dans la gestion des 'Declare ML Module' | notin |
| 2008-03-25 | Interpret patterns for hypotheses types in match goal in type_scope (if not a | msozeau |
| 2008-03-24 | Finish fix in command where we still lost information on what was a type | msozeau |
| 2008-03-23 | Fix examples in Program documentation and add comindexes for the various | msozeau |
| 2008-03-23 | Fix a bug found by B. Grégoire when declaring morphisms in module | msozeau |
| 2008-03-23 | Nettoyage Wf.v et unification (suite remarques faites sur cocorico) | herbelin |
| 2008-03-23 | Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards. | herbelin |
| 2008-03-23 | Une passe sur les réels: | herbelin |
| 2008-03-23 | CoqIDE default font set to monospace so as indentation to be meaningful | herbelin |
| 2008-03-22 | Compatibility fixes, backtrack on definitions of reflexive, | msozeau |
| 2008-03-21 | One more AVL reorganisation: separate pure functions from proofs + functional... | letouzey |
| 2008-03-21 | Correct bug introduced in r10589, where we lost information that | msozeau |
| 2008-03-21 | Some "if then else" instead of orb and andb, in order to vm_compute lazily | letouzey |
| 2008-03-20 | Add a flag to control rewriting under lambdas. Otherwise makes some | msozeau |
| 2008-03-20 | Installation des .vo nécessaire à BigQ | notin |
| 2008-03-20 | Correction d'un bug sur les modules de la forme: | soubiran |
| 2008-03-20 | still some useless invariants in FSetAVL | letouzey |
| 2008-03-19 | some references to IntMap forgotten in last commit | letouzey |
| 2008-03-19 | migration of the old IntMap library from StdLib to a user contrib (Cachan/Int... | letouzey |
| 2008-03-19 | Coq.Relations.Relations can move back to its short name | letouzey |
| 2008-03-19 | Do another pass on the typeclasses code. Correct globalization of class | msozeau |
| 2008-03-19 | tactique gappa | filliatr |
| 2008-03-19 | Various improvements of coqdep, resulting in a big speedup | letouzey |
