aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2018-10-08Merge PR #8554: Fixes #8553: regression of tactic "change" under binders.Pierre-Marie Pédrot
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-04Merge PR #7361: Towards selecting "best" unification failure among severalPierre-Marie Pédrot
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04test-suite: rename a few filesVincent Laporte
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-10-03Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the com...Théo Zimmermann
2018-10-02Move the compat-update-process to right after branchingJason Gross
2018-10-02Update the -compat flagsJason Gross
2018-10-02Update compat notations to be compat 8.7Jason Gross
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-10-02Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0Pierre-Marie Pédrot
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
2018-09-28Merge PR #262: A cleaning step in using heuristics for inference of the retur...Pierre-Marie Pédrot
2018-09-28Merge PR #8479: Fix #8478: Undeclared universe anomaly with sectionsPierre-Marie Pédrot
2018-09-27Possible abstractions over goal variables when inferring match return clause.Hugo Herbelin
2018-09-27Trying an abstracting dependencies heuristic for the match return clause even...Hugo Herbelin
2018-09-27Trying a no-inversion no-dependency heuristic for match return clause.Hugo Herbelin
2018-09-27Inference of return clause: giving uniformly priority to "small inversion".Hugo Herbelin
2018-09-27Unification failure: don't give preference to a "beyond capabilities" error.Hugo Herbelin
2018-09-27Scheme Equality: support for working in a context of Parameters.Hugo Herbelin
2018-09-27Fixing a typo in a comment.Hugo Herbelin
2018-09-27Fixing #4859 (anomaly with Scheme called on inductive type with indices).Hugo Herbelin
2018-09-27Fixing #4612 (anomaly with Scheme called on unsupported inductive type).Hugo Herbelin
2018-09-27Fix #8478: Undeclared universe anomaly with sectionsGaëtan Gilbert
2018-09-27Fixes #8553 (regression of tactic "change" under binders).Hugo Herbelin
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-26[ocaml] Update required OCaml version to 4.05.0Emilio Jesus Gallego Arias
2018-09-26Merge PR #8504: Allow successive attributes #[foo] #[bar]Vincent Laporte
2018-09-26Merge PR #8506: [ssr] use the right environment in ssrpattern (fix #8454)Maxime Dénès
2018-09-26Merge PR #8534: Checking if low-level name printers are used on purpose or notMaxime Dénès
2018-09-26Merge PR #7309: Made names of existential variables interpretable as Ltac var...Pierre-Marie Pédrot
2018-09-26Merge PR #8419: Remove romega in favor of liaThéo Zimmermann
2018-09-26Allow successive attributes #[foo] #[bar]Gaëtan Gilbert
2018-09-26Combined Scheme tests sort to use either "*" or "/\"Théo Winterhalter
2018-09-26Merge PR #8217: Fixes #8215: "critical" type inference bug in interpreting ev...Pierre-Marie Pédrot
2018-09-25Merge PR #8535: Fixing #8532: regression in Print Assumptions within a functor.Pierre-Marie Pédrot
2018-09-25Fixing #8532 (regression in Print Assumptions within a functor).Hugo Herbelin
2018-09-25Remove romegaVincent Laporte
2018-09-24Fixes #8215 ("critical" bug of type inference in interpreting evars by names).Hugo Herbelin
2018-09-24Merge PR #8464: Fix numeral notationsHugo Herbelin
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-21Merge pull request #8462 from vbgl/zify-colonequalLaurent Théry
2018-09-21Merge PR #8455: Move tests in bugs/ to bugs/closed/.Théo Zimmermann
2018-09-21Remove hash based univ level compareGaëtan Gilbert
2018-09-21Add test for univ names of polymorphic inductives in sections.Gaëtan Gilbert
2018-09-21Universe binders are Id, not Name. Never print Var.Gaëtan Gilbert
2018-09-21Best-effort hack to provide a meaningful name for anonymous bound universes.Pierre-Marie Pédrot
2018-09-21Removing calls to AUContext.instance.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 01:41:34 +0000