aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-09-24Merge PR #10774: Make `zify` does work for `Z.to_N`Frédéric Besson
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
2019-09-16Fix #10757: Program Fixpoint uses "exists" for telescopesGaëtan Gilbert
2019-09-16Re-implementation of zifyFrédéric Besson
2019-09-16Remove library-specific code for `Import`.Maxime Dénès
2019-09-09[stdlib] Do not put INR_eq in the “real” hint databaseVincent Laporte
2019-09-04Merge PR #10577: Fix #7348: extraction of dependent record projectionsMaxime Dénès
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-02Merge PR #10719: Make SSR congr tactic work on arrows in Type.Enrico Tassi
2019-09-02Merge PR #10648: [extraction] Fix #7191: Avoid unsound eta-reductionMaxime Dénès
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-08-30Make SSR congr tactic work on arrows in Type.Andreas Lynge
2019-08-29Solve universe error with SSR 'rewrite !term'Andreas Lynge
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-08-26Test-suite fixes from HugoMatthieu Sozeau
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-16Fix Print Assumptions: Inductive types can have unsafe fixpoints orSimonBoulier
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add a file for typing_flags in the test-suite.SimonBoulier
2019-08-10[extraction] Fix #7191: Avoid unsound eta-reductionKazuhiko Sakaguchi
2019-08-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-08-09Merge PR #10641: Fix regression of #10637 (-emacs arg should set color to `EM...Emilio Jesus Gallego Arias
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-08-08Merge PR #10324: Fix #10088: Ltac2 & operator conflicts with notations involv...Maxime Dénès
2019-07-31Fix #7348: extraction of dependent record projectionsKazuhiko Sakaguchi
2019-07-29Use the precondition of diveucl_21 to avoid massaging the dividend.Guillaume Melquiond
2019-07-29Add test from #10551.Guillaume Melquiond
2019-07-29Add a test for #10088.Pierre-Marie Pédrot
2019-07-25Mark primitives integer as able to participate in reductions (fixes #10560).Guillaume Melquiond
2019-07-24Merge PR #10536: Fix #10533: uncaught Invalid_argument Array.fold_left2 in re...Enrico Tassi
2019-07-23Merge PR #10541: Dune: fix build_all_stdlib ruleEmilio Jesus Gallego Arias
2019-07-22Merge PR #10441: Attach the universe polymorphic status to sections.Gaëtan Gilbert
2019-07-22[Pretyping] Do not use the stale evarmap (in thin_evars)Vincent Laporte
2019-07-21Dune: fix build_all_stdlib ruleGaëtan Gilbert
2019-07-19Fix #10533: uncaught Invalid_argument Array.fold_left2 in rewriteGaëtan Gilbert
2019-07-18Polymorphism attribute on section sets the option locally.Pierre-Marie Pédrot
2019-07-18Attach the universe polymorphic status to sections.Pierre-Marie Pédrot
2019-07-03Merge PR #10419: [api] Refactor most of `Decl_kinds`Gaëtan Gilbert
2019-07-02[test-suite] Fix evil plugin after changes in declare API.Emilio Jesus Gallego Arias
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ...Kazuhiko Sakaguchi
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
2019-06-26Merge PR #10401: Fix printers testEmilio Jesus Gallego Arias
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
2019-06-25Give a functional type to Ltac1 quotations with a context.Pierre-Marie Pédrot
2019-06-25Adding the ability to transfer Ltac2 variables to Ltac1 quotations.Pierre-Marie Pédrot
2019-06-25Merge PR #10162: Fix #10161: occur check when defining an algebraic universe.Pierre-Marie Pédrot
2019-06-25Merge PR #10412: Add output-coqtop test directory that runs output tests with...Enrico Tassi
2019-06-24[test-suite] Fix printers testGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 21:38:04 +0000