aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-09-10profondeur maximalefilliatr
2008-09-09added comments in esubst.mlibarras
2008-09-09Correction bug assert (introduit dans la révision 11300) qui neherbelin
2008-09-09Suppression d'un warning inutilenotin
2008-09-09Fix a bug reintroduced in [setoid_reflexivity] etc...msozeau
2008-09-07Commit fixes from v8.2 branch (r11386 and r11387)glondu
2008-09-07Generalize usage of $(FIND_VCS_CLAUSE) and add debian to itglondu
2008-09-07Do not install csdpcert in $(BINDIR)glondu
2008-09-07Check [Equations] patterns are for the right function.msozeau
2008-09-07Add the ability to declare [Hint Extern]'s with no pattern.msozeau
2008-09-07Fixes in typeclasses resolution. Avoid reducing instances types beforemsozeau
2008-09-07Update CHANGES and INSTALLglondu
2008-09-07Add some calls to $(STRIP) for consistencyglondu
2008-09-07$(DLLCOQRUN) is not an executableglondu
2008-09-07Small fixes in "varify", a small tactic doing the first part ofmsozeau
2008-09-07Skip complexity tests on demandglondu
2008-09-07More debugging of [Equations], now able to discharge even the heavilymsozeau
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-09-06Install coqide manpageglondu
2008-09-06Install dllcoqrun.so and use it by defaultglondu
2008-09-06More cleaningglondu
2008-09-06Create the bin/ directory if non-existentglondu
2008-09-06Always use environment variablesglondu
2008-09-06$(COQLIB) -> $(COQLIBINSTALL) in Makefilesglondu
2008-09-06Use $(COQTOPEXE) to refer to bin/coqtop in Makefilesglondu
2008-09-05Report 11364 de 8.2 vers trunk (bugs affichage Print Module)herbelin
2008-09-05Parametrize link flags for VM-dependent bytecodeglondu
2008-09-05Build coqrun library using ocamlmklib...glondu
2008-09-04Correction du bug #1908 (améliorations de coqdoc.css)notin
2008-09-04Improve typeclasses eauto using the dnet for local assumptions too, and selectmsozeau
2008-09-04Correction du bug #1937notin
2008-09-04Rely on ocamlc to call the C compiler...glondu
2008-09-04Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anmsozeau
2008-09-03Better handling of recursive Equations definitions... still not perfect.msozeau
2008-09-03Fix bug #1935, reworking the reflexivity, symmetry... tactics to usemsozeau
2008-09-03Correct handling of implicit arguments in [Equations] definitions,msozeau
2008-09-02Add support for recursive definitions to [Equations], deciding if amsozeau
2008-09-02Initial implementation of a new command to define (dependent) functions bymsozeau
2008-09-02- Remove some dead code in subtacmsozeau
2008-09-02fixed minor environment issues when checking inductive typesbarras
2008-09-02fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...barras
2008-09-02added Makefile target: validate (to recheck all .vo in a row)barras
2008-09-02avoid small overflowsbarras
2008-09-02[checker] basic conversion oracle: expand local vars firstbarras
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-08-27Fix implementation of "Global Instance" which redeclared the samemsozeau
2008-08-27Major speed and space improvements in setoid rewrite:msozeau
2008-08-27Little cleanup in auto.msozeau
2008-08-26Give back progress information after feeding the Program Instance to themsozeau
2008-08-23Fix dependency problem that makes compilation fail :)msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-02 21:18:29 +0000