aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2019-12-11Merge PR #11271: Fixing #9893. "Specialize with" would not support hyps type ...Pierre-Marie Pédrot
2019-12-10Merge PR #10202: Slightly more robust manual implicit argumentsEmilio Jesus Gallego Arias
2019-12-10Fixing #9893 (Letins not supported in the specialized hypothesis).Pierre Courtieu
2019-12-05Unfortunate bug with "cofix with": case of a CProdN over no bindings.Hugo Herbelin
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
2019-12-03Merge PR #11113: Remove deprecated compat modifier of Notation / Infix commands.Emilio Jesus Gallego Arias
2019-12-03Merge PR #11162: [CS] support #[local] attributeMaxime Dénès
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-12-01Merge PR #11185: Remove deprecated Typeclasses Axioms Are Instances.Gaëtan Gilbert
2019-11-29Remove deprecated Typeclasses Axioms Are Instances.Théo Zimmermann
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-13Return of Refine Instance as an attribute.Gaëtan Gilbert
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-10-30[test-suite] Test section-local mutual Fixpoint.Emilio Jesus Gallego Arias
2019-10-30Merge PR #10973: Remove dead code in save_remaining_recthmsEmilio Jesus Gallego Arias
2019-10-27Merge PR #10827: Replace classical reals quotient axioms by functional extens...Hugo Herbelin
2019-10-26Remove dead code in save_remaining_recthmsGaëtan Gilbert
2019-10-24Replace classical reals quotient axioms by functional extensionality. Define ...Vincent Semeria
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
2019-09-18Merge PR #9856: A 'zify' tactic as a ML pluginMaxime Dénès
2019-09-16Re-implementation of zifyFrédéric Besson
2019-09-16Remove library-specific code for `Import`.Maxime 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-10Make rewrite use the registered elimination schemesAndreas Lynge
2019-07-18Attach the universe polymorphic status to sections.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-09Merge PR #8726: More robust treatment of the Discharge statusPierre-Marie Pédrot
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-05-23Fixing typos - Part 3JPR
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to p...Enrico Tassi
2019-05-10Use Print Custom Grammar to inspect custom entriesJasper Hugunin
2019-05-10[Attributes] Allow explicit value for two-valued attributesVincent Laporte
2019-05-07Merge PR #10016: [test-suite] Remove a test with a Timeout that fails frequen...Vincent Laporte
2019-05-03Tactics: fixing "change_no_check in".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 11:37:24 +0000