aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact thatGravatar msozeau2009-04-20
* Fix bug #2089: correctly dealing with parameters and real arguments inGravatar msozeau2009-04-16
* Fix and actually beautify the bug script to adapt to the new measureGravatar msozeau2009-04-14
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* - Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingGravatar herbelin2009-04-08
* Add tests for quoteGravatar glondu2009-03-30
* Avoid inadvertent declaration of "on" as a keyword. New syntax isGravatar msozeau2009-03-29
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Fixes in Program well-founded definitions:Gravatar msozeau2009-03-26
* coq_makefile: -c and -shared conflict; tacinterp: delay evaluation of tactic ...Gravatar barras2009-03-19
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* illegal tactic application was having Ltac interpreter loopGravatar barras2009-03-04
* Add support for dependent "destruct" over terms in dependent types.Gravatar herbelin2009-02-23
* commited complexity test for exponential behavior of unificationGravatar barras2009-02-09
* Fixing #2044 (bad printing of primitive notation at the head ofGravatar herbelin2009-02-06
* From v8.2 to trunk:Gravatar herbelin2009-02-06
* Report r11631 from 8.2 and handle non-dependent goals better inGravatar msozeau2009-02-04
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
* Fixing bug #1918 (no occur-check in Meta unification was done yet!).Gravatar herbelin2009-01-20
* - Fixing bug 1891 (abusive instantiations of evar arguments inGravatar herbelin2009-01-20
* The initial state evar numbering increased. Fix output message in a test.Gravatar puech2009-01-19
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
* - Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).Gravatar herbelin2009-01-11
* Uniformisation of some error messages + added test on setoid rewrite.Gravatar herbelin2009-01-07
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* Regression test for bug #1967Gravatar herbelin2009-01-02
* Conséquence renommage canonique de refl_equal en eq_refl.Gravatar herbelin2009-01-02
* - Fixed bug #2021 (uncaught exception with injection/discriminate whenGravatar herbelin2009-01-01
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* Fix for syntax changes in test-suite scripts.Gravatar msozeau2008-12-16
* About "apply in":Gravatar herbelin2008-12-09
* improved simplGravatar barras2008-12-03
* Add new directory for pre-compilation of files needed for further tests.Gravatar herbelin2008-12-02
* Miscellaneous fixes and improvements:Gravatar herbelin2008-12-02
* fixed kernel bug (de Bruijn) + test-suiteGravatar barras2008-12-02
* Test case for previous commit.Gravatar msozeau2008-11-27
* fixed bug 1791: simpl was performing eta expansionGravatar barras2008-11-27
* added tests for hyps reorderingGravatar barras2008-11-27
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
* Fixed bug #2006 (type constraint on Record was not taken into account) +Gravatar herbelin2008-11-23
* Add missing test-suite files for closed bugs.Gravatar msozeau2008-11-14
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 85f007b7-540e-0...Gravatar barras2008-11-13
* - Correction erreur dans test output Notation.vGravatar herbelin2008-11-09
* Add test-suite file related to discussion of syntax of implicit binders.Gravatar msozeau2008-11-09
* Slight change of the semantics of user-given casts: they don't reallyGravatar msozeau2008-11-07
* - Ajout possibilité de lancer ocamldebug sur coqideGravatar herbelin2008-11-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 13:59:27 +0000