aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
2019-01-24Add some quot/rem test-cases for niaJason Gross
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...Jason Gross
2019-01-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
2019-01-24Add subst to the end of nia in the test-suiteJason Gross
2019-01-24Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanupJason Gross
2019-01-24Remove remainder of `Abort`s in test-suite Nia.vJason Gross
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2018-12-30Fixing an interpretation bug of the "in" clause of "match".Hugo Herbelin
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-19Merge PR #9001: [options] Remove deprecated option automatic introduction.Pierre-Marie Pédrot
2018-11-18[options] Remove deprecated option automatic introduction.Emilio Jesus Gallego Arias
2018-11-16Do not Export the init modulesGaëtan Gilbert
2018-11-12Do not qualify universe names by section path.Gaëtan Gilbert
2018-11-12Fix incorrect coq-prog-args in unideclsGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 10:04:58 +0000