| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2008-09-06 | Use $(COQTOPEXE) to refer to bin/coqtop in Makefiles | glondu |
| 2008-09-05 | Report 11364 de 8.2 vers trunk (bugs affichage Print Module) | herbelin |
| 2008-09-05 | Parametrize link flags for VM-dependent bytecode | glondu |
| 2008-09-05 | Build coqrun library using ocamlmklib... | glondu |
| 2008-09-04 | Correction du bug #1908 (améliorations de coqdoc.css) | notin |
| 2008-09-04 | Improve typeclasses eauto using the dnet for local assumptions too, and select | msozeau |
| 2008-09-04 | Correction du bug #1937 | notin |
| 2008-09-04 | Rely on ocamlc to call the C compiler... | glondu |
| 2008-09-04 | Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving an | msozeau |
| 2008-09-03 | Better handling of recursive Equations definitions... still not perfect. | msozeau |
