aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-10-04Allow SProp default onGaëtan Gilbert
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive projec...Frédéric Besson
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-10-01Remove spurious uses of CoInductive in SSR prerequisite.Pierre-Marie Pédrot
2019-09-25Merge PR #10784: Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindPierre-Marie Pédrot
2019-09-25Merge PR #10781: Fixes #10778 (fresh was not updated after renaming of introp...Pierre-Marie Pédrot
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-24Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindGaëtan Gilbert
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-23Fixes #10778 (fresh was not updated after renaming of intropattern entry in #...Hugo Herbelin
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
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-10[ssr] Add test "do [under ... do ...] in H"Erik Martin-Dorel
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-08-08[ssr] under: Add a contrived example to test under/over with SetoidsErik Martin-Dorel
2019-08-08[ssr] Refactor under's Setoid generalization to ease stdlib2 portingErik Martin-Dorel
2019-08-06[ssr] under: extend ssreflect.v to generalize iff to any setoid eqErik Martin-Dorel
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 16:36:45 +0000