aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2010-10-05test-suite: fix success/AdvancedCanonicalStructure.vglondu
2010-10-05Export definition of type implicits_list for contribs + fixed aherbelin
2010-10-05test-suite: use unified diff output and use expected output as referenceglondu
2010-10-04Fixing bugs in previous commits about implicit arguments:herbelin
2010-10-03Test for non-regression of the display bug fixed in r13486.herbelin
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-10-03Making display of various informations about constants more modular:herbelin
2010-09-30Improve handling of metas as evars in unification (patch by Hugo)letouzey
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
2010-09-20Fixed test of bug #2360 (use of Fail to check a regular error insteadherbelin
2010-09-19Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weherbelin
2010-09-18Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inherbelin
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-09-17Fixed a problem introduced in r12607 after pattern_of_constr servedherbelin
2010-09-17In the computation of missing arguments for apply, accept that theherbelin
2010-09-11Improving a few error messages in Ltac interpretationherbelin
2010-09-02fixed bug #2375 (congruence)corbinea
2010-07-30Updated test on Nsatz after Loïc moved NsatzR to Nsatz.herbelin
2010-07-29test-case for bug #2105barras
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
2010-07-28fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-05 08:24:24 +0000