aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
2019-02-19Notations: Fixing a printing bug with patterns.Hugo Herbelin
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-13[ssr] move shorter Canonical to Coq properEnrico Tassi
2019-02-13Merge PR #9557: [ssreflect] Export more parsing witnesses.Enrico Tassi
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2019-02-11[ssreflect] Export more parsing witnesses.Emilio Jesus Gallego Arias
2019-02-11[ssr] keep user annotation on views (fix #9538)Enrico Tassi
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08locus: Add an AtLeastOneOccurrence constructor.Matthieu Sozeau
2019-02-08Merge PR #9410: Make `Program` a regular attributeMatthieu Sozeau
2019-02-06Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.Théo Zimmermann
2019-02-05Unset the Ltac backtrace printing by default.Pierre-Marie Pédrot
2019-02-05Add an option not to register Ltac backtraces.Pierre-Marie Pédrot
2019-02-05Make Program a regular attributeMaxime Dénès
2019-02-04Primitive integersMaxime Dénès
2019-02-04Merge PR #9291: Do not take universes into account in lia reification.Frédéric Besson
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:06:44 +0000