| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2008-09-10 | profondeur maximale | filliatr |
| 2008-09-09 | added comments in esubst.mli | barras |
| 2008-09-09 | Correction bug assert (introduit dans la révision 11300) qui ne | herbelin |
| 2008-09-09 | Suppression d'un warning inutile | notin |
| 2008-09-09 | Fix a bug reintroduced in [setoid_reflexivity] etc... | msozeau |
| 2008-09-07 | Commit fixes from v8.2 branch (r11386 and r11387) | glondu |
| 2008-09-07 | Generalize usage of $(FIND_VCS_CLAUSE) and add debian to it | glondu |
| 2008-09-07 | Do not install csdpcert in $(BINDIR) | glondu |
| 2008-09-07 | Check [Equations] patterns are for the right function. | msozeau |
| 2008-09-07 | Add the ability to declare [Hint Extern]'s with no pattern. | msozeau |
| 2008-09-07 | Fixes in typeclasses resolution. Avoid reducing instances types before | msozeau |
| 2008-09-07 | Update CHANGES and INSTALL | glondu |
| 2008-09-07 | Add some calls to $(STRIP) for consistency | glondu |
| 2008-09-07 | $(DLLCOQRUN) is not an executable | glondu |
| 2008-09-07 | Small fixes in "varify", a small tactic doing the first part of | msozeau |
| 2008-09-07 | Skip complexity tests on demand | glondu |
| 2008-09-07 | More debugging of [Equations], now able to discharge even the heavily | msozeau |
| 2008-09-07 | Better handling of the opacity of proof obligations, add the possibility of | msozeau |
| 2008-09-06 | Install coqide manpage | glondu |
| 2008-09-06 | Install dllcoqrun.so and use it by default | glondu |
| 2008-09-06 | More cleaning | glondu |
| 2008-09-06 | Create the bin/ directory if non-existent | glondu |
| 2008-09-06 | Always use environment variables | glondu |
| 2008-09-06 | $(COQLIB) -> $(COQLIBINSTALL) in Makefiles | glondu |
