aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-07-21Backporting fix to bug #2353 (fixpoint with recursively non-uniformherbelin
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
2010-07-12Fix compilation and test-suite of nsatzglondu
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 01:28:49 +0000