aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
2020-04-15[declare] Rename `Declare.t` to `Declare.Proof.t`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Pfedit` into proofs.Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
2020-04-15Merge PR #11776: [ocamlformat] Enable for funind.Pierre Courtieu
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-11[dune] [stdlib] Build the standard library natively with Dune.Emilio Jesus Gallego Arias
2020-04-10Merge PR #11756: [lib] Remove custom backtrace-destroying finalizersPierre-Marie Pédrot
2020-04-10[ocamlformat] Enable for funind.Emilio Jesus Gallego Arias
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-02Merge PR #12002: Cleanup tactic_option a bitPierre-Marie Pédrot
2020-04-02Cleanup tactic_option a bitGaëtan Gilbert
2020-04-01[lib] Remove custom backtrace destroying finalizersEmilio Jesus Gallego Arias
2020-03-31Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit ...Hugo Herbelin
2020-03-31Merge PR #11915: [proof] Split delayed and regular proof closing functionsPierre-Marie Pédrot
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-31Merge PR #11823: [funind] [cleanup] Remove unused function parametersPierre-Marie Pédrot
2020-03-31[declare] [rewrite] Use high-level declare API, part II.Emilio Jesus Gallego Arias
2020-03-31[declare] [rewrite] Use high-level declare API, part I.Emilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
2020-03-30[declareDef] More consistent handling of universe bindersEmilio Jesus Gallego Arias
2020-03-30[declare] Make the type of closed entries opaque.Emilio Jesus Gallego Arias
2020-03-30[ComDefinition] Split program from regular declarationsEmilio Jesus Gallego Arias
2020-03-30[proof] Miscellaneous cleanup on proof info handlingEmilio Jesus Gallego Arias
2020-03-31Merge PR #11647: [rfc] Consolidation of parsing interfacesPierre-Marie Pédrot
2020-03-30ocamlformat: use whitelist instead of blacklistGaëtan Gilbert
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-27Merge PR #11848: Nicer printing for decimal constantsHugo Herbelin
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-25[ocamlformat] Use doc-comments=before style.Emilio Jesus Gallego Arias
2020-03-25Nicer printing for decimal constants in RPierre Roux
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-22Adding bignat to parse positive numbers; bigint now includes negative ints.Hugo Herbelin
2020-03-22Merge PR #11731: [proof] Miscellaneous refactoringsGaëtan Gilbert
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-20Merge PR #11847: Properly thread let-bindings in Funind principle construction.Pierre Courtieu
2020-03-20Merge PR #11857: Remove calls to structural equality in MicromegaVincent Laporte
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 20:15:53 +0000