aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13- Do not make constants with an assigned type polymorphic (wrong unfoldings).msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
2011-04-08Fixing multiple printing bugs with "Notation f x := ..."herbelin
2011-03-31Did that adding a rule for printing applications as "f(x)" works.herbelin
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
2011-03-16Adapt test-suite/output/Extraction_matchs_2413 to new indentation of extractionletouzey
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
2011-03-05Starting being more explicit on the reasons why module subtyping fails.herbelin
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
2011-02-22Try to fix the behavior of clenv_missing used when declaring hintsletouzey
2011-02-21Some fixes of the test-suite scriptsletouzey
2011-02-21Fix test-suite script.msozeau
2011-02-10MacOS compatibilitypboutill
2011-02-08Correct handling of existential variables when multiple differentmsozeau
2011-01-27test-suite/Makefile: add a rule to build all_stdlib.v (for the bench)glondu
2011-01-25Add a test for sorting all universes of stdlibglondu
2011-01-11Add "Print Sorted Universes"glondu
2011-01-07Fixing an uncaught exception bug with use of vmcastherbelin
2010-12-23Remove the two-argument variant of "decide equality"glondu
2010-12-21Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)letouzey
2010-12-19Fixing bug #2454: inversion predicate strategy for inferring the typeherbelin
2010-12-04Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).herbelin
2010-12-03Fixing bug using explictly declared implicit arguments in inductive arities.herbelin
2010-12-02Fixing a bug introduced in r12304 (move of interpretation ofherbelin
2010-11-19SearchAbout: who has never been annoyed by the [ ] syntax ?letouzey
2010-10-31An experimental support for open constrs in hints and in "using"herbelin
2010-10-16Fix missing -coqlib argument to coqdep in test-suiteglondu
2010-10-12Adding test-case for bug #2362, which uses HO unification duringmsozeau
2010-10-12Fix bug #2393: allow let-ins inside telescopes (only fails when there'smsozeau
2010-10-11Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingherbelin
2010-10-07test-suite: fix success/unification.vglondu
2010-10-06test-suite: fix output/Existentials.outglondu
2010-10-05test-suite: fix success/Typeclasses.vglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 16:09:38 +0000