aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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-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-19Move tests in bugs/ to the bugs/closed/.Nick Lewycky
2018-09-19Fix Numeral Notations (4/4 - fixing synch)Jason Gross
2018-09-19[ssr] use the right environment in ssrpattern (fix #8454)Enrico Tassi
2018-09-19Fix #7754: universe declarations on mutual inductivesGaëtan Gilbert
2018-09-19Merge PR #8341: Reduce universe redeclarations (catching AlreadyDeclared)Matthieu Sozeau
2018-09-18Zify: replace local definitions by equationsVincent Laporte
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
2018-09-14Merge PR #7894: Remove quote pluginThéo Zimmermann
2018-09-14Merge PR #8326: Mention PRINT_LOGS=1 when failing test suiteEnrico Tassi
2018-09-13Add test for inconsistency from polymorphism capturing global univsGaëtan Gilbert
2018-09-13Add option to control automatic template polymorphism.Gaëtan Gilbert
2018-09-13Add explicit atribute for template polymorphism.Gaëtan Gilbert
2018-09-13Mention PRINT_LOGS=1 when failing test suiteGaëtan Gilbert
2018-09-13Move test suite report script to standalone script fileGaëtan Gilbert
2018-09-12Remove quote pluginMaxime Dénès
2018-09-12Merge PR #8243: Remove xargs from "make clean" so it won't fail on CygwinEnrico Tassi
2018-09-12Merge PR #8433: Fix bug #8432 : program fixpoint and universesPierre-Marie Pédrot
2018-09-11Made names of existential variables interpretable as Ltac variables.Hugo Herbelin
2018-09-11Merge PR #7288: Isolating ltac naming out of pretyping + fixing renamingPierre-Marie Pédrot
2018-09-11Merge PR #8285: Fixing #8270: cbn was applying zeta even when not asked for.Pierre-Marie Pédrot
2018-09-11Merge PR #7135: Introducing an explicit `Declare Scope` commandEmilio Jesus Gallego Arias
2018-09-10Merge PR #8417: Fixing #8416: Print Assumptions missing module information fr...Matthieu Sozeau
2018-09-10Merge PR #8290: Fix #8288: cumulativity inferance ignores args to bound varia...Matthieu Sozeau
2018-09-10Adapting standard library to the introduction of "Declare Scope".Hugo Herbelin
2018-09-10Fixing ltac names interpretation in internals of pattern-matching compilation.Hugo Herbelin
2018-09-10Fixing an inconsistency in interpreting Ltac names linking to binder names.Hugo Herbelin
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-09-07Fix bug #8432 : program fixpoint and universesMatthieu Sozeau
2018-09-06Fixing #8270 (cbn was calling zeta even when not asked for).Hugo Herbelin
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-05Fixing #8416 (Print Assumptions missing module information from compiled files).Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 13:49:30 +0000