aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-01-29Merge PR #9383: Remove travisVincent Laporte
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
2019-01-27[test] for bug #9385Enrico Tassi
2019-01-27Merge PR #9214: Notations: Removing useless parentheses on abbreviations shor...Emilio Jesus Gallego Arias
2019-01-25Merge PR #8637: Update -compat to support -compat 8.10Théo Zimmermann
2019-01-25Notations: Removing useless parentheses on abbrevs for prefix of an application.Hugo Herbelin
2019-01-24Merge PR #9325: Stop [Print] from saying [is (not) universe polymorphic].Hugo Herbelin
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-24Merge PR #9377: [CS] recognize applied primitive projections as keys (fix #9375)Matthieu Sozeau
2019-01-23Merge PR #9270: Turn `Refine instance Mode` off by defaultPierre-Marie Pédrot
2019-01-23Merge PR #9337: Fixing #9329: registering empty levels in the order they are ...Emilio Jesus Gallego Arias
2019-01-22Remove travisGaëtan Gilbert
2019-01-22Fixing #9329 (registering empty levels in the order they are recomputed).Hugo Herbelin
2019-01-22Make prvect tail recursive (fix #9355)Gaëtan Gilbert
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-22Make `Add Morphism` not rely on Refine InstanceMaxime Dénès
2019-01-22Distinguish ASTs for Instance and Declare InstanceMaxime Dénès
2019-01-22[CS] recognize applied primitive projections as keys (fix #9375)Enrico Tassi
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
2019-01-18[ssr] compile "=> {} y" as "=> {y} y"Enrico Tassi
2019-01-14Merge PR #9307: Handle local definitions in implicit arguments of InstanceMaxime Dénès
2019-01-09Stop [Print] from saying [is (not) universe polymorphic].Gaëtan Gilbert
2019-01-09Make some tests more robust by adding missing proof terminatorsMaxime Dénès
2019-01-09Test ltacprof in sequential modeMaxime Dénès
2019-01-09Make it possible to pass flags to coq when running test suiteMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` p...Maxime Dénès
2019-01-08Merge PR #9292: Fixing some wrong scopes of variables in the interpretation o...Emilio Jesus Gallego Arias
2019-01-07Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constantEnrico Tassi
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
2019-01-04Handle local definitions in implicit arguments of InstanceJasper Hugunin
2018-12-30Fixing an interpretation bug of the "in" clause of "match".Hugo Herbelin
2018-12-26Merge PR #8734: Make diffs work for more input stringsHugo Herbelin
2018-12-25Fixing printing bug due to using equality ill-checking hash key of kernel name.Hugo Herbelin
2018-12-22Merge PR #9248: Fix #7904: update proofview env after ltac constr:()Pierre-Marie Pédrot
2018-12-21Fix #9240: Register for IDProp causes anomaly when non constantGaëtan Gilbert
2018-12-21Do not exclude "opened" bugs from reportMaxime Dénès
2018-12-21Merge PR #9182: Stop printing Monomorphic/Polymorphic in Print.Maxime Dénès
2018-12-20Make diffs work for more input stringsJim Fehrle
2018-12-20Merge PR #8488: Warning when using automatic template polymorphismPierre-Marie Pédrot
2018-12-20Merge PR #9200: [ssr] make `>` stand aloneMaxime Dénès
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
2018-12-19Put #[universes(template)] in outputs testsGaëtan Gilbert
2018-12-19Merge PR #9231: Fixes #9229: Infix not robust wrt choice of variable names in...Pierre-Marie Pédrot
2018-12-18Merge PR #9223: Fix universe restriction in delayed mode.Pierre-Marie Pédrot
2018-12-18[ssr] make > a stand alone intro patternEnrico Tassi
2018-12-18Fixes #9229 (Infix not robust wrt choice of variable names).Hugo Herbelin
2018-12-18[ssr] new test by Arthur CharguéraudEnrico Tassi
2018-12-18[ssr] extended intro patterns: + > [^] /ltac:Enrico Tassi
2018-12-18Merge PR #9222: Fix classification of Set Default Proof Mode.Enrico Tassi
2018-12-18Merge PR #9160: Avoid user-given names in automatic introduction of bindersPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 00:05:42 +0000