aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2011-09-26Added support for referring to subterms of the goal by pattern.herbelin
2011-09-22test-suite : an additional message displayed by Notation2.vletouzey
2011-09-22Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.letouzey
2011-09-19Fix test-suite/ide for repository compiled without -local (fix #2600)letouzey
2011-09-17Various fixes in the Makefilesletouzey
2011-09-15Omega aware of Z.pred (fix #1912)letouzey
2011-09-15Re-allowing assumptions during proofs seems safe now (fix #2411)letouzey
2011-09-06test-suite/ide: misc improvementletouzey
2011-09-05fake_ide: a short program to mimic an ide talking to coqtop -ideslaveletouzey
2011-08-10Fixing printing bug with last trailing non-maximally implicitherbelin
2011-08-10Partly revert commit r14389 about relaxing the condition for being a keywordherbelin
2011-08-08Be a bit less aggressive in declaring idents as keywords in notationsherbelin
2011-08-04moins de reification inutile, noatations standardspottier
2011-07-26or_introl is now too complicated for basic tests of test-suite/output/PrintIn...pboutill
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin
2011-06-22fix bug 2510: xml test is in the summary if it failspboutill
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-18r14204 and 14218 continued: completely removing test for bug #2490,herbelin
2011-06-18Partial backtrack on wrong r14204: bug #2490 still open.herbelin
2011-06-18add names of theorems in outputjnarboux
2011-06-16Tests de nsatz avec la geometriepottier
2011-06-14Regression files for bugs #2304 and #2490.herbelin
2011-06-14Fixing bug #2181 (Class mechanism can create dependencies over unnamedherbelin
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
2011-06-13Another bug of Scheme Induction (generated names dep/nodep were swapped).herbelin
2011-06-13Fixing an anomaly in Scheme Induction.herbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-10Fixing another bug with "_" intro pattern.herbelin
2011-06-10Made use of "_" in repeated use of intros_patterns work (withherbelin
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
2011-06-08Make Notation works with anonymous-level "Type".herbelin
2011-05-26Mini-test for etaherbelin
2011-05-26Partial fix for accepting bound variables with same name as implicitherbelin
2011-05-26Fixing discriminate for identity.herbelin
2011-05-17Add simple test of bullet behaviour.aspiwack
2011-05-16test-suite: no more ..._beq in the output of the search testsletouzey
2011-05-16Fix order in Search tests.letouzey
2011-05-15Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).herbelin
2011-05-06Fixes in the test-suite after modularisation of ZArith and coletouzey
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-04-29Typo in test InitSyntax.outherbelin
2011-04-28Fixing an "apply -> ... in hyp" bug (the hyp was considered as a fixedherbelin
2011-04-28Fixed notation printing bug when curly brackets are involved (requestsherbelin
2011-04-27Fixing output of Notations2.v test messed up in r14060herbelin
2011-04-25Fixing and completing interpretation of let's in notations for iterated binders.herbelin
2011-04-15Take benefit of eta-expansion so that "ex P" is displayed "exists x, P x".herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 20:19:15 +0000