aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
* psatz Z -> psatz Z 1Gravatar fbesson2009-07-30
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Move some examples for groebner into a test-suite fileGravatar letouzey2009-07-20
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
* Adding a regression test about Bauer's example on coq-club ofGravatar herbelin2009-06-02
* Fix script file using the "Manual Implicit" flag.Gravatar msozeau2009-06-02
* micromega: proof compression bugfixGravatar fbesson2009-05-11
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Fix test output mentionning an existential number that changed.Gravatar msozeau2009-04-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 15:02:53 +0000