aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2019-04-23[ssr] under: Move {beta_expand, unify_helper} in the module type (qualify them)Erik Martin-Dorel
2019-04-23[ssr] under: Strenghten over & Add test_big_andbErik Martin-Dorel
2019-04-23[ssr] under: Extend the test-suite to exemplify most use casesErik Martin-Dorel
2019-04-23[ssr] under: generate missing Under subgoal for eq_bigl/eq_bigErik Martin-Dorel
2019-04-23[ssr] under: Add support for one-liners "under (…) by [tac1|tac2]."Erik Martin-Dorel
2019-04-23[ssr] over: also works on universally quantified goalsErik Martin-Dorel
2019-04-23[ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over"Erik Martin-Dorel
2019-04-23[ssr] under: Rename bound variables a posteriori for cosmetic purposeEnrico Tassi
2019-04-02[ssr] rewrite takes optional function to make the new valued of the redexEnrico Tassi
2019-04-02[ssr] implement "under i: ext_lemma" by rewrite ruleEnrico Tassi
2019-04-02[ssr] under: Add opaque modules for tagging and notation supportErik Martin-Dorel
2019-04-02[ssr] fix implementation of refine ~first_goes_lastEnrico Tassi
2019-04-02[ssr] clean up type declaration of ssrrewritetacEnrico Tassi
2019-04-02[ssr] move is_ind/constructor_ref to ssrcommonEnrico Tassi
2019-04-02[ssr] under: rewrite takes an optional bool argErik Martin-Dorel
2019-04-01Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and ...Vincent Laporte
2019-04-01Several improvements and fixes of LiaFrédéric Besson
2019-03-31Multiple payload types in tokensPierre Roux
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
2019-03-27[funind] Try to be more precise with universe contexts in recdef hooks.Emilio Jesus Gallego Arias
2019-03-27[geninterp] Track polymorphic status in tactic interpretation.Emilio Jesus Gallego Arias
2019-03-27[vernac] Allow path for `save_proof` where no proof state is present.Emilio Jesus Gallego Arias
2019-03-27[plugins] [funind] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [extraction] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [derive] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [setoid_ring] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [micromega] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[plugins] [ssr] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27[coqpp] [ltac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-26Merge PR #9489: [ssr] avoid HO unification to perform truncation analysy in elimMaxime Dénès
2019-03-25[ssr] Use Coqlib in “abstract”Vincent Laporte
2019-03-25[ssr] More detailed error message in rewriteVincent Laporte
2019-03-25[ssr] avoid HO unif when doing truncation analysisEnrico Tassi
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-20Merge PR #9770: Correct dependencies in the micromega packEmilio Jesus Gallego Arias
2019-03-15Merge PR #8817: SProp: the definitionally proof irrelevant universePierre-Marie Pédrot
2019-03-14Fix various dummy Relevant in ssrGaëtan Gilbert
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Exposes Coq_micromega.dump_proof_term to allow a use independent from tacticsChantal Keller
2019-03-14Correct dependencies in the micromega packChantal Keller
2019-03-12Merge PR #9389: Implement a method for manual declaration of implicits.Emilio Jesus Gallego Arias
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-03-06Merge PR #9476: Constructor type information uses the expanded form.Gaëtan Gilbert
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-28Fix #7632: Change syntax of autoapply according to the documentation.Théo Zimmermann
2019-02-28Implement a method for manual declaration of implicits.Jasper Hugunin
2019-02-23[vernac] Unify declaration hooks.Emilio Jesus Gallego Arias
2019-02-19Merge PR #9297: Two fixes in printing notations with patternsEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 08:38:03 +0000