aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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-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-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
2018-09-10Fixing ltac names interpretation in internals of pattern-matching compilation.Hugo Herbelin
2018-09-10Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.Hugo Herbelin
2018-09-03Merge PR #8387: Make -compat 8.8 import Coq.Compat.Coq88Théo Zimmermann
2018-09-03Merge PR #8064: Numeral notation (revisited again)Hugo Herbelin
2018-09-02Make -compat 8.8 import Coq.Compat.Coq88Jason Gross
2018-08-31Give a proper error message on num-not in functorJason Gross
2018-08-31Add some module tests to numeral notationsJason Gross
2018-08-31Make Numeral Notation obey Local/GlobalJason Gross
2018-08-31Make Numeral Notation follow Import, not RequireJason Gross
2018-08-31[numeral notations] support aliasesJason Gross
2018-08-31Add Numeral Notation GlobRef printing/parsingJason Gross
2018-08-31Add a warning about abstract after being a no-opJason Gross
2018-08-31Update doc and test-suite after supporting univ polyJason Gross
2018-08-31Fix numeral notation for a rebase on top of masterJason Gross
2018-08-30[ssr] move ssr_*v tests to test-suite/ssr/Enrico Tassi
2018-08-27Update test-suite for focusing on named goals.Théo Zimmermann
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29A test on the different ways to indicate the levels of a rule.Hugo Herbelin
2018-07-24Add simple test cases for vm and native on primitive projections.Gaëtan Gilbert
2018-07-17Remove fourier pluginMaxime Dénès
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-07-03[test suite] Test case for attributesVincent Laporte
2018-07-03Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commandsPierre-Marie Pédrot
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-07-01Add test for Uniform Inductive ParametersJasper Hugunin
2018-06-24Adding various tests for mutual records.Pierre-Marie Pédrot
2018-06-19Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsPierre-Marie Pédrot
2018-06-15Add test-suite case for performance, had to use TimeoutMatthieu Sozeau
2018-06-15Better elaboration of pattern-matchings on primitive projectionsMatthieu Sozeau
2018-06-15Do not allow spliting in res_pf, this is reserved for pretypingMatthieu Sozeau
2018-06-04Merge PR #7229: Deprecate implicit tactic solving.Hugo Herbelin
2018-06-04Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.Matthieu Sozeau
2018-06-04Deprecate implicit tactic solving.Pierre-Marie Pédrot
2018-05-17Introduce an option to allow nested lemma, and turn it off by default.Théo Zimmermann
2018-05-02Make "intro"/"intros" progress on existential variables.Hugo Herbelin
2018-04-29Strict focusing using Default Goal Selector.Gaëtan Gilbert
2018-04-26Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 07:52:59 +0000