aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2019-10-22Merge PR #10880: Allow to pass Ltac1 values to Ltac2 quotations.Jason Gross
2019-10-22Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in th...Pierre-Marie Pédrot
2019-10-22Merge PR #10886: test-suite/Makefile: work when manually involved for dune-co...Enrico Tassi
2019-10-21Merge PR #10857: Fix votour after the change of representation of opaques.Maxime Dénès
2019-10-21Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.Hugo Herbelin
2019-10-21Merge PR #10863: Minor side effect universe cleanupsPierre-Marie Pédrot
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
2019-10-19Don't abort in test for #6323.Gaëtan Gilbert
2019-10-18Merge PR #10914: Fix Locate printing regressionHugo Herbelin
2019-10-18Adding a test for votour.Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
2019-10-17Fix Locate printing regressionGuillaume Melquiond
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
2019-10-14Fix #9851: anomaly when unsolved evar in Add RingGaëtan Gilbert
2019-10-14test-suite/Makefile: work when manually involved for dune-compiled CoqGaëtan Gilbert
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-13Fix #10888: Context import behaviour in modtypeGaëtan Gilbert
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-05Fix #10669 incorrect substitution in context outside sectionGaëtan Gilbert
2019-10-04Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint data...Pierre-Marie Pédrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ...Pierre-Marie Pédrot
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 16:54:55 +0000