aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2019-04-30Mini-test.Hugo Herbelin
2019-04-28[test-suite] Remove a test with a Timeout that fails frequently on CI.Théo Zimmermann
2019-04-16Fix spurious argument of {measure}Maxime Dénès
2019-04-16Take advantage of relaxed {measure} syntax in test suiteMaxime Dénès
2019-04-06Fix numeral notations test in async mode.Gaëtan Gilbert
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
2019-04-02Remove -compat 8.7Jason Gross
2019-04-02Add a Numeral Notation for QArith (e.g., 1.02e+01%Q for 102 # 10)Pierre Roux
2019-04-02Make R parser parse decimals (e.g., 1.02e+01)Pierre Roux
2019-04-01Add test-case for #9840Jason Gross
2019-03-18[kernel] Fix compare_head_gen_leq_with to use [leq] on applicationsMatthieu Sozeau
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Enable proof irrelevance for SProp.Gaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-22Apply implicit binders to Hypothesis inside sections.Jasper Hugunin
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
2019-02-04Primitive integersMaxime Dénès
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 00:46:22 +0000