aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-02-08Resolve #10342 : [Ltac2] Add array libraryMichael Soegtrop
2020-02-06Merge PR #10835: Accepting a few more variants of format for recursive notati...Pierre-Marie Pédrot
2020-02-05Add --fuzz, --real, --user to timing scriptsJason Gross
2020-02-04Correct bug in non max local implicit argumentsSimonBoulier
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-02-04Merge PR #11513: Test for #5617: Primitive projections confuse the terminatio...Gaëtan Gilbert
2020-02-04Fix #11515: Ltac2 rewrite on wildcard.Pierre-Marie Pédrot
2020-02-04Merge PR #11514: add regression test for liaPierre-Marie Pédrot
2020-02-03add regression test for liaAndres Erbsen
2020-02-03Test for #5617: Primitive projections confuse the termination checker.Pierre-Marie Pédrot
2020-02-03Fix efficiency regression #11436Frédéric Besson
2020-01-31More tolerant in format for recursive notations.Hugo Herbelin
2020-01-30Printing tests for applied references combined with impl. args. and notations.Hugo Herbelin
2020-01-29Merge PR #11399: Checker: use inductive's check_template flagPierre-Marie Pédrot
2020-01-29Merge PR #11472: Fix #11467 ('e' was not displayed when printing decimal nota...Pierre-Marie Pédrot
2020-01-28docs: Add missing prefix (bug_*.v)Erik Martin-Dorel
2020-01-28Fix #11467Pierre Roux
2020-01-27Checker: use inductive's check_template flagGaëtan Gilbert
2020-01-27schemes: use rigid universesGaëtan Gilbert
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
2020-01-19Merge PR #11348: Discharge inductive types without rechecking themPierre-Marie Pédrot
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
2020-01-15Merge PR #11373: Close #11168Pierre-Marie Pédrot
2020-01-15Merge PR #11374: Close #11133Pierre-Marie Pédrot
2020-01-15Discharge inductive types without rechecking themGaëtan Gilbert
2020-01-14Merge PR #11394: [coqdoc] Fix #11353: coqdoc -g omits all sentences with deco...Hugo Herbelin
2020-01-14[coqdoc] Fix #11353: coqdoc -g omits all sentences with decorationsKarl Palmskog
2020-01-14Merge PR #10486: [extraction] Support extraction of Coq's string type to OCam...Kazuhiko Sakaguchi
2020-01-13Merge PR #11285: fix #11279. Specialize h no longer expands letins in the typ...Pierre-Marie Pédrot
2020-01-13Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...Pierre-Marie Pédrot
2020-01-12fix #11279. Specialize h no longer expands letins in the type of h.Pierre Courtieu
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Add test case for string extraction in OCaml and HaskellMaxime Dénès
2020-01-08Close #11133Gaëtan Gilbert
2020-01-08replace deprecated -quick with -vio in the test suiteEnrico Tassi
2020-01-08Close #11168Gaëtan Gilbert
2020-01-08Merge PR #11341: Add non-utf8 timing testPierre-Marie Pédrot
2020-01-07Merge PR #11245: [tools] Remove support for python2Théo Zimmermann
2020-01-07Fix test-suite fo non maximal implicit argumentsSimonBoulier
2020-01-06Fix #11140: Bidirectionality hints perform (surprising?) simplificationMaxime Dénès
2020-01-06[micromega] fix of bug #11191Frédéric Besson
2020-01-06Merge PR #11361: Fix #11360: discharge of template inductive with param only ...Pierre-Marie Pédrot
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2020-01-04Fixing status reporting for complexity tests.Hugo Herbelin
2020-01-03Merge PR #11343: fix: Shorten ssrsetoid.v to fix TC performance issueEnrico Tassi
2020-01-03coq_makefile: test with CAMLPKGS and mllibGaëtan Gilbert
2020-01-03[tools] Remove support for python2Emilio Jesus Gallego Arias
2019-12-30Merge PR #11233: Fixes #11231: missing dependency in looking for default clau...Pierre-Marie Pédrot
2019-12-29Merge PR #11334: Fixes a small bug exposing an _ANONYMOUS_REL in a unificatio...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 03:35:02 +0000