aboutsummaryrefslogtreecommitdiff
path: root/test-suite/failure
AgeCommit message (Expand)Author
2020-07-01UIP in SPropGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-01-27Checker: use inductive's check_template flagGaëtan Gilbert
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-02-04Primitive integersMaxime Dénès
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04test-suite: rename a few filesVincent Laporte
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-09Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesMaxime Dénès
2018-03-08Fix SR breakage due to allowing fixpoints on non-rec valuesMatthieu Sozeau
2018-02-27Update headers following #6543.Théo Zimmermann
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2017-04-11Update various comments to use "template polymorphism"Gaetan Gilbert
2016-03-25Test suite file for a bug in int31 arithmetic fixed a while ago.Maxime Dénès
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Fix test-suite fileMatthieu Sozeau
2015-06-24Extend test-suite for the positivity checker.Arnaud Spiwack
2015-01-12Update headers.Maxime Dénès
2014-07-22Add test-suite file for guard condition on cofixpoints.Maxime Dénès
2014-04-09Add another critical bug to the test-suite.Maxime Dénès
2014-01-15Test case containing a proof of false due to a DeBruijn off-by-one error in theMaxime Dénès
2013-12-21Test case for the buggy commutative cut subterm rule.Maxime Dénès
2013-12-17test guard condition against feature incompatible with prop-extBruno Barras
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Matthieu Sozeau
2013-09-20Fix name clash in "failure/inductive.v".xclerc
2013-09-20Merge "circular_subtyping?.v" tests into a single "circular_subtyping.v" test.xclerc
2013-09-20Merge "inductive?.v" tests into a single "inductive.v" test.xclerc
2013-09-20Use "Fail" rather than rely on exit code.xclerc
2013-09-19Uminus.v : prepare this test file for the use of Failletouzey
2013-09-19universes-buraliforti-redef.v : repair a match after Pierre B. syntax changesletouzey
2013-01-18Unset Asymmetric Patternspboutill
2012-08-08Updating headers.herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2011-10-05Fixing critical inductive polymorphism bug found by Bruno.herbelin
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-20Added examples for checking that the guard condition excludes subtermsherbelin
2010-03-24Fixed bug #2260 (check of resolution of all evars in the declarationherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-08Fixed a bug introduced in revision 12265.herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-11Relatively ad hoc fix to an ill-typed instantiation bug in typeherbelin
2008-12-02fixed kernel bug (de Bruijn) + test-suitebarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:31:56 +0000