aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-09-07Fix bug #8432 : program fixpoint and universesMatthieu Sozeau
2018-09-06Merge PR #8302: Fix #7795: UGraph.AlreadyDeclared with ProgramMatthieu Sozeau
2018-09-06Merge PR #8295: Fix #8291: print universe names in universe context for Check.Matthieu Sozeau
2018-09-05Merge PR #7968: Restrict universes in comInductiveGaëtan Gilbert
2018-09-03Merge PR #8387: Make -compat 8.8 import Coq.Compat.Coq88Théo Zimmermann
2018-09-03Merge PR #8064: Numeral notation (revisited again)Hugo Herbelin
2018-09-03Merge PR #891: Check universes are declaredGaëtan Gilbert
2018-09-03Merge PR #8124: Fix #8121: anomalies in native_compute with let and evars.Maxime Dénès
2018-09-03Merge PR #8359: [ssr] move ssr_*v tests to test-suite/ssr/Maxime Dénès
2018-09-03Merge PR #8107: Fixes #8106: anomaly if declaring levels for only printing th...Emilio Jesus Gallego Arias
2018-09-03Merge PR #8286: Fixing #7867: class error message tried to print a "fun" with...Emilio Jesus Gallego Arias
2018-09-02Make -compat 8.8 import Coq.Compat.Coq88Jason Gross
2018-09-02Fixing #7867 (class error message tries to print a "fun" with no binder).Hugo Herbelin
2018-09-02Fixing #8106 (anomaly if declaring levels for only printing then only parsing).Hugo Herbelin
2018-08-31Give a proper error message on num-not in functorJason Gross
2018-08-31Add some module tests to numeral notationsJason Gross
2018-08-31Make Numeral Notation obey Local/GlobalJason Gross
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
2018-08-31[numeral notations] support aliasesJason Gross
2018-08-31Add Numeral Notation GlobRef printing/parsingJason Gross
2018-08-31Add a warning about abstract after being a no-opJason Gross
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
2018-08-31Fix numeral notation for a rebase on top of masterJason Gross
2018-08-31WIP: adapt Numeral Notation to synchronized prim notationsPierre Letouzey
2018-08-31Numeral Notation + test-suite : fix 3 tests using Datatypes.v but not Prelude.vPierre Letouzey
2018-08-31prim notations backtrackable, their declarations now in two parts (API change)Pierre Letouzey
2018-08-30[ssr] move ssr_*v tests to test-suite/ssr/Enrico Tassi
2018-08-29Merge PR #8167: Fix ordering of before/after in print-pretty-timed-*Enrico Tassi
2018-08-28Close #8091: print universe context for Eval when option on.Gaëtan Gilbert
2018-08-28Fix #8291: print universe names in universe context for Check.Gaëtan Gilbert
2018-08-28Fix #7795: UGraph.AlreadyDeclared with ProgramGaëtan Gilbert
2018-08-27Update test-suite for focusing on named goals.Théo Zimmermann
2018-08-24Fix ordering of before/after in print-pretty-timed-*Jason Gross
2018-08-06Add regression test for issue #4202Tej Chajed
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-29A test on the different ways to indicate the levels of a rule.Hugo Herbelin
2018-07-27[ci] Remove CircleCI setup.Emilio Jesus Gallego Arias
2018-07-26Add information to option type errorsTej Chajed
2018-07-26Fix #8121: anomalies in native_compute with let and evars.Pierre-Marie Pédrot
2018-07-26Merge PR #8122: Fix #8119: anomalies in vm_compute with let and evars.Maxime Dénès
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...Pierre-Marie Pédrot
2018-07-26Merge PR #7274: Avoiding introducing dependency on the indices of a term whic...Pierre-Marie Pédrot
2018-07-25Fix #7900 previous commit fixes a bug when using side effects in obligations.Matthieu Sozeau
2018-07-25Merge PR #8133: Fixes #8126: issue with notations and nested applicationsEmilio Jesus Gallego Arias
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2018-07-25Optimized dependencies for pattern-matching on only trivial patterns.Hugo Herbelin
2018-07-24Fix #8119: anomalies in vm_compute with let and evars.Pierre-Marie Pédrot
2018-07-24Add simple test cases for vm and native on primitive projections.Gaëtan Gilbert
2018-07-24Fix #7329: coqchk Include with primitive projectionsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:20:03 +0000