| Age | Commit message (Expand) | Author |
|---|
| 2008-10-18 | Optimisation de clenv.ml pour que meta_instance ne soit pas appelé | herbelin |
| 2008-10-18 | Expérience de simplification de Ndigits compte tenu des tactiques existant | herbelin |
| 2008-10-18 | - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429) | herbelin |
| 2008-10-18 | Que Time n'empêche pas la colorisation des mots-clés. | herbelin |
| 2008-10-18 | Intégration et formattage du développement de Pierre Castéran sur les | herbelin |
| 2008-10-17 | Suppression de la dépendance de install-doc envers doc : | notin |
| 2008-10-16 | Extraction of Module with eq = ... : fix for bug #1853 | letouzey |
| 2008-10-16 | Extraction of mutual types with alias: fix for bug #1965 | letouzey |
| 2008-10-16 | Attempt to clarify Extract_env.extract_seb_spec | letouzey |
| 2008-10-15 | Report des commits 11417 et 11437 de la v8.2 | soubiran |
| 2008-10-14 | report de la révision r11451 (nouveau style html pour le manuel de référence) | notin |
| 2008-10-14 | Dumpglob.dump_modref : fix an assert failure | letouzey |
| 2008-10-14 | test-suite: more utf8 tests, a test of ! ? and so on in rewrites | letouzey |
| 2008-10-14 | ugly comment erroneously left in the minus definition | letouzey |
| 2008-10-11 | Backporting 11445 from 8.2 to trunk (negative conditions in | herbelin |
| 2008-10-09 | * Fixed constr_cmp again to handle universes subtyping correctly | puech |
| 2008-10-08 | Fix bug #1959 (remember: never use a partial functions mindlessly). | msozeau |
| 2008-10-08 | Améliorations de l'affichage des coercions suggérées par Georges : | herbelin |
| 2008-10-07 | fixing r11433 again: | barras |
| 2008-10-07 | fixed pb with r11433 | barras |
| 2008-10-06 | bug #1951: polymorphic indtypes: universe subst was not performed in the type... | barras |
| 2008-10-06 | ## Lines starting with '## ' will be removed from the log message. | msozeau |
| 2008-10-03 | (Try to) use the conversion oracle also in w_unify to choose which constant to | msozeau |
| 2008-10-03 | Minor fixes related to coqdoc and --interpolate and the dependent | msozeau |
| 2008-10-02 | Fixing constr_cmp, propagating subtyping only right of a product | puech |
| 2008-09-30 | Correcting a delta normalization bug in VM (checked by benjamin) | jforest |
| 2008-09-25 | Forgot one file. | msozeau |
| 2008-09-25 | Improvements in coqdoc: | msozeau |
| 2008-09-25 | Various little improvements: | msozeau |
| 2008-09-25 | Partial fix for bug #1948: recompute order of dependencies between | msozeau |
| 2008-09-16 | Report change of the implicit argument status of the carrier type in the | msozeau |
| 2008-09-15 | Report improvements in Equations to the dependent elimination tactic: | msozeau |
| 2008-09-15 | Fix bug #1943 and restrict the inference optimisation of Program to | msozeau |
| 2008-09-15 | Add types introduced by subtac in *.glob files | glondu |
| 2008-09-15 | Update stdlib html template | glondu |
| 2008-09-14 | A pass on documentation: | msozeau |
| 2008-09-14 | Add user syntax for creating hint databases [Create HintDb foo | msozeau |
| 2008-09-14 | Use manual implicts in Classes and rationalize class parameter names. | msozeau |
| 2008-09-14 | In manual implicit arguments mode, do not enrich implicits | msozeau |
| 2008-09-14 | Fix bug #1931 by searching for a sort after doing beta,iota,delta- | msozeau |
| 2008-09-14 | Fix bug #1936: uncaught exception due to undefinable exceptions. | msozeau |
| 2008-09-14 | Fix bug #1939: defined evars were not substituted in some typeclasses | msozeau |
| 2008-09-14 | Fix bug #1940: uncaught exception when searching for a type class. | msozeau |
| 2008-09-13 | Finish debugging the unification machinery in [Equations]. Do the _comp | msozeau |
| 2008-09-13 | Remove redefinition of id in Program.Basics, just add maximal implicits. | msozeau |
| 2008-09-13 | Fix a bug, in fold_constr_with_binders, the types of fixpoints were | msozeau |
| 2008-09-12 | Add a type argument to letin_tac instead of using casts and recomputing | msozeau |
| 2008-09-11 | Fixes in dependent induction tactic, putting things in better order for | msozeau |
| 2008-09-11 | Add enough information to correctly globalize recursive calls in inductive and | msozeau |
| 2008-09-11 | Some more debugging of [Equations], unification still not perfect. | msozeau |
