aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-02-04[dune] Fix Dune build in Windows.Emilio Jesus Gallego Arias
2019-02-04Merge PR #6914: Primitive integersPierre-Marie Pédrot
2019-02-04Merge PR #9317: Restrict universes in records.Pierre-Marie Pédrot
2019-02-04Primitive integersMaxime Dénès
2019-02-04Merge PR #9368: Discard argument names of section variables on section closePierre-Marie Pédrot
2019-02-04Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.Maxime Dénès
2019-02-04Merge PR #9426: [test-suite] Fix display of check.Enrico Tassi
2019-02-04Merge PR #9454: Fix off-by-one error in nat syntax warningsPierre-Marie Pédrot
2019-02-04Merge PR #9452: [proof] optimize proof always works on incomplete proofsPierre-Marie Pédrot
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
2019-02-02Merge PR #9250: coqchk: fix check for kelim with functorsPierre-Marie Pédrot
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2019-01-31Fix off-by-one error in nat syntax warningsJason Gross
2019-01-31add testEnrico Tassi
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-30Restrict universes in records.Gaëtan Gilbert
2019-01-29Update update-compat.py scriptJason Gross
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
2019-01-29[test-suite] Display full paths on CHECK.Emilio Jesus Gallego Arias
2019-01-29Merge PR #9383: Remove travisVincent Laporte
2019-01-29[test-suite] Fix display of check.Emilio Jesus Gallego Arias
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-24Add some quot/rem test-cases for niaJason Gross
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...Jason Gross
2019-01-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
2019-01-24Add subst to the end of nia in the test-suiteJason Gross
2019-01-24Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanupJason Gross
2019-01-24Remove remainder of `Abort`s in test-suite Nia.vJason Gross
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
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-20Discard argument names of section variables on section closeJasper Hugunin
2019-01-19[ssr] compile "=> {x..} y" as "=> {x..y} y"Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:29:49 +0000