aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Add a type argument to letin_tac instead of using casts and recomputingGravatar msozeau2008-09-12
* Fixes in dependent induction tactic, putting things in better order forGravatar msozeau2008-09-11
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Some more debugging of [Equations], unification still not perfect.Gravatar msozeau2008-09-11
* profondeur maximaleGravatar filliatr2008-09-10
* added comments in esubst.mliGravatar barras2008-09-09
* Correction bug assert (introduit dans la révision 11300) qui neGravatar herbelin2008-09-09
* Suppression d'un warning inutileGravatar notin2008-09-09
* Fix a bug reintroduced in [setoid_reflexivity] etc...Gravatar msozeau2008-09-09
* Commit fixes from v8.2 branch (r11386 and r11387)Gravatar glondu2008-09-07
* Generalize usage of $(FIND_VCS_CLAUSE) and add debian to itGravatar glondu2008-09-07
* Do not install csdpcert in $(BINDIR)Gravatar glondu2008-09-07
* Check [Equations] patterns are for the right function.Gravatar msozeau2008-09-07
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* Update CHANGES and INSTALLGravatar glondu2008-09-07
* Add some calls to $(STRIP) for consistencyGravatar glondu2008-09-07
* $(DLLCOQRUN) is not an executableGravatar glondu2008-09-07
* Small fixes in "varify", a small tactic doing the first part ofGravatar msozeau2008-09-07
* Skip complexity tests on demandGravatar glondu2008-09-07
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
* Better handling of the opacity of proof obligations, add the possibility ofGravatar msozeau2008-09-07
* Install coqide manpageGravatar glondu2008-09-06
* Install dllcoqrun.so and use it by defaultGravatar glondu2008-09-06
* More cleaningGravatar glondu2008-09-06
* Create the bin/ directory if non-existentGravatar glondu2008-09-06
* Always use environment variablesGravatar glondu2008-09-06
* $(COQLIB) -> $(COQLIBINSTALL) in MakefilesGravatar glondu2008-09-06
* Use $(COQTOPEXE) to refer to bin/coqtop in MakefilesGravatar glondu2008-09-06
* Report 11364 de 8.2 vers trunk (bugs affichage Print Module)Gravatar herbelin2008-09-05
* Parametrize link flags for VM-dependent bytecodeGravatar glondu2008-09-05
* Build coqrun library using ocamlmklib...Gravatar glondu2008-09-05
* Correction du bug #1908 (améliorations de coqdoc.css)Gravatar notin2008-09-04
* Improve typeclasses eauto using the dnet for local assumptions too, and selectGravatar msozeau2008-09-04
* Correction du bug #1937Gravatar notin2008-09-04
* Rely on ocamlc to call the C compiler...Gravatar glondu2008-09-04
* Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anGravatar msozeau2008-09-04
* Better handling of recursive Equations definitions... still not perfect.Gravatar msozeau2008-09-03
* Fix bug #1935, reworking the reflexivity, symmetry... tactics to useGravatar msozeau2008-09-03
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
* Add support for recursive definitions to [Equations], deciding if aGravatar msozeau2008-09-02
* Initial implementation of a new command to define (dependent) functions byGravatar msozeau2008-09-02
* - Remove some dead code in subtacGravatar msozeau2008-09-02
* fixed minor environment issues when checking inductive typesGravatar barras2008-09-02
* fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...Gravatar barras2008-09-02
* added Makefile target: validate (to recheck all .vo in a row)Gravatar barras2008-09-02
* avoid small overflowsGravatar barras2008-09-02
* [checker] basic conversion oracle: expand local vars firstGravatar barras2008-09-02
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* Fix implementation of "Global Instance" which redeclared the sameGravatar msozeau2008-08-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 01:05:54 +0000