aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 14:01:17 +0000