aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2018-11-07Revert "Do not allow spliting in res_pf, this is reserved for pretyping"Enrico Tassi
2018-11-05Merge PR #8515: Command driven attributesPierre-Marie Pédrot
2018-11-02Remove incorrect is_universe_polymorphism from modinternGaëtan Gilbert
2018-11-02Make attributes more general to make defining #[universes(...)] easyGaëtan Gilbert
2018-10-31No need to require List in test-suite/success/Inductive.vGaëtan Gilbert
2018-10-15Correct some spelling errorsBenjamin Barenblat
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-08Merge PR #8630: Some cleaning in the test suiteEnrico Tassi
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04test-suite: rename a few filesVincent Laporte
2018-10-02Update the -compat flagsJason Gross
2018-10-01Merge PR #7634: Extend combined scheme to Schemes in TypeMatthieu Sozeau
2018-09-28Merge PR #262: A cleaning step in using heuristics for inference of the retur...Pierre-Marie Pédrot
2018-09-27Possible abstractions over goal variables when inferring match return clause.Hugo Herbelin
2018-09-27Trying an abstracting dependencies heuristic for the match return clause even...Hugo Herbelin
2018-09-27Trying a no-inversion no-dependency heuristic for match return clause.Hugo Herbelin
2018-09-27Scheme Equality: support for working in a context of Parameters.Hugo Herbelin
2018-09-27Fixing a typo in a comment.Hugo Herbelin
2018-09-26Merge PR #8504: Allow successive attributes #[foo] #[bar]Vincent Laporte
2018-09-26Merge PR #7309: Made names of existential variables interpretable as Ltac var...Pierre-Marie Pédrot
2018-09-26Allow successive attributes #[foo] #[bar]Gaëtan Gilbert
2018-09-26Combined Scheme tests sort to use either "*" or "/\"Théo Winterhalter
2018-09-25Remove romegaVincent Laporte
2018-09-21Merge pull request #8462 from vbgl/zify-colonequalLaurent Théry
2018-09-18Zify: replace local definitions by equationsVincent Laporte
2018-09-14Fixing yet a source of dependency on alphabetic order in unification.Hugo Herbelin
2018-09-13Add option to control automatic template polymorphism.Gaëtan Gilbert
2018-09-13Add explicit atribute for template polymorphism.Gaëtan Gilbert
2018-09-11Made names of existential variables interpretable as Ltac variables.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 04:29:56 +0000