| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2008-09-03 | Fix bug #1935, reworking the reflexivity, symmetry... tactics to use | msozeau |
| 2008-09-03 | Correct handling of implicit arguments in [Equations] definitions, | msozeau |
| 2008-09-02 | Add support for recursive definitions to [Equations], deciding if a | msozeau |
| 2008-09-02 | Initial implementation of a new command to define (dependent) functions by | msozeau |
| 2008-09-02 | - Remove some dead code in subtac | msozeau |
| 2008-09-02 | fixed minor environment issues when checking inductive types | barras |
| 2008-09-02 | fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp... | barras |
| 2008-09-02 | added Makefile target: validate (to recheck all .vo in a row) | barras |
| 2008-09-02 | avoid small overflows | barras |
| 2008-09-02 | [checker] basic conversion oracle: expand local vars first | barras |
| 2008-09-02 | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about | herbelin |
| 2008-08-27 | Fix implementation of "Global Instance" which redeclared the same | msozeau |
| 2008-08-27 | Major speed and space improvements in setoid rewrite: | msozeau |
| 2008-08-27 | Little cleanup in auto. | msozeau |
| 2008-08-26 | Give back progress information after feeding the Program Instance to the | msozeau |
| 2008-08-23 | Fix dependency problem that makes compilation fail :) | msozeau |
| 2008-08-22 | - New auto hints for transparency/opacity control, not bound to | msozeau |
| 2008-08-22 | Typo (corrige le bug #1928) | notin |
| 2008-08-21 | Fixes in dependent induction tactic to keep names, allow giving | msozeau |
| 2008-08-21 | Various fixes w.r.t typeclasses and subtac: resolve tcs properly inside | msozeau |
| 2008-08-18 | Revert commit 11326, to see if it is what makes bench fail | glondu |
