aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
...
* 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
* Add some example uses of the new record features in Record.v:Gravatar msozeau2008-11-07
* Fix a bug in the specialization by unification tactic related to the problemsGravatar msozeau2008-11-07
* Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)Gravatar herbelin2008-11-04
* test-suite/ideal-features/{apply.v -> eapply_evar.v}Gravatar glondu2008-11-02
* 11511 continued (bug in set.out + incohérence dans "Theorem with"Gravatar herbelin2008-10-28
* - Fixed many "Theorem with" bugs.Gravatar herbelin2008-10-27
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Retour en arrière pour raison de compatibilité sur la suppression du nf_evar Gravatar herbelin2008-10-19
* - Merge modifs coq_makefile.ml4 de la 8.1 vers le trunk (commit 11429)Gravatar herbelin2008-10-18
* test-suite: more utf8 tests, a test of ! ? and so on in rewritesGravatar letouzey2008-10-14
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
* Report change of the implicit argument status of the carrier type in theGravatar msozeau2008-09-16
* Report improvements in Equations to the dependent elimination tactic:Gravatar msozeau2008-09-15
* Fix bug #1931 by searching for a sort after doing beta,iota,delta-Gravatar msozeau2008-09-14
* Finish debugging the unification machinery in [Equations]. Do the _compGravatar msozeau2008-09-13
* 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
* Some more debugging of [Equations], unification still not perfect.Gravatar msozeau2008-09-11
* Skip complexity tests on demandGravatar glondu2008-09-07
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
* 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
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* Renaming parser -> coq-parserGravatar glondu2008-08-18
* micromega : bug fixes and optimisationsGravatar fbesson2008-08-07
* Correction de bugs:Gravatar herbelin2008-08-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Oops... the trunk behaviour is differentGravatar glondu2008-07-29
* Update test-suite outputGravatar glondu2008-07-29