aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-07-19Merge PR #7941: Extend QuestionMark to produce a better error message in case...Pierre-Marie Pédrot
2018-07-18Merge PR #8054: [dev] Autogenerate OCaml dev files.Enrico Tassi
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-07-12[dev] Autogenerate OCaml dev files.Emilio Jesus Gallego Arias
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-09Merge PR #7884: Fix #5719: Uncaught exception Invalid_argument.Matthieu Sozeau
2018-07-06Add test for #8004.Gaëtan Gilbert
2018-07-04Convert timing tools to run with both python2 and python3Jasper Hugunin
2018-07-03[test suite] Test case for attributesVincent Laporte
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-01Add test for Uniform Inductive ParametersJasper Hugunin
2018-07-01Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation f...Emilio Jesus Gallego Arias
2018-06-29Workaround to fix #7731 (printing not splitting line at break hint).Hugo Herbelin
2018-06-29Fixes #7712 (an anomaly in reporting bad recursive notation format).Hugo Herbelin
2018-06-28Merge PR #7860: Fix #7704: Launching coqide through PATH fails.Emilio Jesus Gallego Arias
2018-06-28Merge PR #7866: Implementation of mutual records in the higher strataMaxime Dénès
2018-06-27Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)Pierre-Marie Pédrot
2018-06-27Test file for #7723Maxime Dénès
2018-06-26Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).Hugo Herbelin
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Matthieu Sozeau
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-25Merge PR #7620: [ssr] rewrite: turn anomaly into regular errorMaxime Dénès
2018-06-24Adding various tests for mutual records.Pierre-Marie Pédrot
2018-06-23Merge PR #7236: [ssr] simpler semantics for delayed clearsMaxime Dénès
2018-06-22Fix #7704: get_toplevel_path needs normalised argv.(0)Gaëtan Gilbert
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-22[ssr] implement {}/v as a short hand for {v}/v when v is an idEnrico Tassi
2018-06-22[ssr] test case for rewrite and set on univ poly keysEnrico Tassi
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2018-06-20[ssr] test case for rewrite (setoid) making the goal illtypedEnrico Tassi
2018-06-19Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsPierre-Marie Pédrot
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-17Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related t...Pierre-Marie Pédrot
2018-06-17Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretypingPierre-Marie Pédrot
2018-06-17Fixes #7811 (uncaught Not_found in notation printer related to "match").Hugo Herbelin
2018-06-17Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Maxime Dénès
2018-06-15Add test-suite case for performance, had to use TimeoutMatthieu Sozeau
2018-06-15Better elaboration of pattern-matchings on primitive projectionsMatthieu Sozeau
2018-06-15Do not allow spliting in res_pf, this is reserved for pretypingMatthieu Sozeau
2018-06-14Workaround to handle non-value arguments in tactics.Cyprien Mangin
2018-06-14Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Pierre-Marie Pédrot
2018-06-14Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...Matthieu Sozeau
2018-06-14Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...Matthieu Sozeau
2018-06-14Merge PR #7771: Tweak printing boxes for unicode bindersHugo Herbelin
2018-06-13Markdown docs: switch from absolute to relative links.Théo Zimmermann
2018-06-12Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Hugo Herbelin
2018-06-12Fixes #7780 (missing lift in expanding alias under a binder in unification).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 19:09:21 +0000