aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Fixing new bug introduced in r14665 when fixing bug #1834.Gravatar herbelin2011-11-17
* Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).Gravatar herbelin2011-11-16
* Suppression fichier Case8.v redondantGravatar herbelin2011-11-16
* Improved check is_open_canonical_projectionGravatar gareuselesinge2011-11-08
* Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsGravatar letouzey2011-11-07
* Fixing incorrect change to pattern-unification over Meta's introducedGravatar herbelin2011-11-06
* Fixing tactic remember not correctly checking preservation of typingGravatar herbelin2011-11-06
* Regression tests for bugs #2613 and #2616.Gravatar herbelin2011-10-25
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Fixing "destruct" test.Gravatar herbelin2011-10-25
* New strategy to infer return predicate of match construct whenGravatar herbelin2011-10-25
* Mod_subst: Attempt to fix #2608Gravatar letouzey2011-10-24
* Fixing another bug revealing ill-typed use of evar restriction.Gravatar herbelin2011-10-24
* Use full conversion for checking type of holes in destruct over aGravatar herbelin2011-10-22
* Fix bug #2473 due to wrong folding of the evar environmentGravatar msozeau2011-10-18
* Fix inductive coercion code in Program (bug #2378)Gravatar msozeau2011-10-18
* Fix bug #2586 and enhance clsubst* as well as a side effectGravatar msozeau2011-10-18
* Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...Gravatar msozeau2011-10-17
* test-suite: non-regression test for bug #2603Gravatar letouzey2011-10-12
* Added test for bug #2615Gravatar herbelin2011-10-11
* Completing r14538 (Chung-Kil Hur's trick for fast dependently-typedGravatar herbelin2011-10-11
* fsetdec : non-atomic elements are now transformed as variables first (fix #2464)Gravatar letouzey2011-10-07
* Improved handling of element equalities in fsetdec (fix #2467)Gravatar letouzey2011-10-07
* Fixing critical inductive polymorphism bug found by Bruno.Gravatar herbelin2011-10-05
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* Added support for referring to subterms of the goal by pattern.Gravatar herbelin2011-09-26
* test-suite : an additional message displayed by Notation2.vGravatar letouzey2011-09-22
* Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.Gravatar letouzey2011-09-22
* Fix test-suite/ide for repository compiled without -local (fix #2600)Gravatar letouzey2011-09-19
* Various fixes in the MakefilesGravatar letouzey2011-09-17
* Omega aware of Z.pred (fix #1912)Gravatar letouzey2011-09-15
* Re-allowing assumptions during proofs seems safe now (fix #2411)Gravatar letouzey2011-09-15
* test-suite/ide: misc improvementGravatar letouzey2011-09-06
* fake_ide: a short program to mimic an ide talking to coqtop -ideslaveGravatar letouzey2011-09-05
* Fixing printing bug with last trailing non-maximally implicitGravatar herbelin2011-08-10
* Partly revert commit r14389 about relaxing the condition for being a keywordGravatar herbelin2011-08-10
* Be a bit less aggressive in declaring idents as keywords in notationsGravatar herbelin2011-08-08
* moins de reification inutile, noatations standardsGravatar pottier2011-08-04
* or_introl is now too complicated for basic tests of test-suite/output/PrintIn...Gravatar pboutill2011-07-26
* This adds two option tables 'Printing Record' and 'Printing Constructor'Gravatar herbelin2011-07-16
* fix bug 2510: xml test is in the summary if it failsGravatar pboutill2011-06-22
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* r14204 and 14218 continued: completely removing test for bug #2490,Gravatar herbelin2011-06-18
* Partial backtrack on wrong r14204: bug #2490 still open.Gravatar herbelin2011-06-18
* add names of theorems in outputGravatar jnarboux2011-06-18
* Tests de nsatz avec la geometrieGravatar pottier2011-06-16
* Regression files for bugs #2304 and #2490.Gravatar herbelin2011-06-14
* Fixing bug #2181 (Class mechanism can create dependencies over unnamedGravatar herbelin2011-06-14
* Added full pattern-unification on Meta for tactic unification.Gravatar herbelin2011-06-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 17:24:33 +0000