aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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
2019-01-31Merge PR #8720: [Numeral notations] Use Coqlib registered constantsEmilio Jesus Gallego Arias
2019-01-29Merge PR #9274: Make `Instance` without a body always open a proofEnrico Tassi
2019-01-28Merge PR #9341: [ssr] uniform clear disciplineMaxime Dénès
2019-01-25[Numeral notations] Lazy resolution of decimal typesVincent Laporte
2019-01-25[Numeral notations] Use Coqlib registered constantsVincent Laporte
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...Jason Gross
2019-01-24Move cleanup from the test-suite to Z.div_mod_to_quot_rem_cleanupJason Gross
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
2019-01-24Don't pose any disjunctions in div_mod_to_quot_remJason Gross
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2019-01-24Merge PR #9269: Move and rewrite intro pattern sectionThéo Zimmermann
2019-01-23Move and rewrite documentation for intro patterns that was underJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:52:04 +0000