aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
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
2018-04-16Merge PR #7237: [ssr] fix delayed clears (fix #7045)Maxime Dénès
2018-04-13[ltac] Deprecate nameless fix/cofix.Emilio Jesus Gallego Arias
2018-04-13[ssr] fix delayed clears (fix #7045)Enrico Tassi
2018-04-12Merge PR #7087: Congruence tactic engine updatePierre-Marie Pédrot
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-29Fix #6770: fixpoint loses locality info in proof mode.Gaëtan Gilbert
2018-03-27Congruence: Fixing a bug with native projections.Hugo Herbelin
2018-03-09Fix expected number of arguments for cumulative constructors.Gaëtan Gilbert
2018-03-09Merge PR #6775: Allow using cumulativity without forcing strict constraints.Maxime Dénès
2018-03-09Cumulativity: improve treatment of irrelevant universes.Gaëtan Gilbert
2018-03-09Allow using cumulativity without forcing strict constraints.Gaëtan Gilbert
2018-03-09added test for coercion from typecharguer
2018-03-09allow Prop as source for coercionscharguer
2018-03-09Merge PR #6747: Relax conversion of constructors according to the pCuIC modelMaxime Dénès
2018-03-08Merge PR #6522: Fix core hint database issue #6521Maxime Dénès
2018-03-08Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish...Maxime Dénès
2018-03-08Add test-suite file for cumulative constructorsMatthieu Sozeau
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-03-06An experimental 'Show Extraction' command (grant feature wish #4129)Pierre Letouzey
2018-03-06[compat] Remove "Shrink Abstract"Emilio Jesus Gallego Arias
2018-03-06Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ...Maxime Dénès
2018-03-06Merge PR #6896: [compat] Remove NOOP deprecated options.Maxime Dénès
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04[compat] Remove NOOP and alias deprecated options.Emilio Jesus Gallego Arias
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04Merge PR #935: Handling evars in the VMMaxime Dénès
2018-03-03Adding a test file for evar handling in the VM.Pierre-Marie Pédrot
2018-03-01Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 12:49:08 +0000