aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2020-05-03[funind] Remove use of low-level entries in scheme generation.Emilio Jesus Gallego Arias
2020-05-03[funind] Make `build_functional_principle` use a functional evar_mapEmilio Jesus Gallego Arias
2020-05-02Move tclWRAPFINALLY to profile_ltacJason Gross
2020-05-02Decrease LtacProf overhead when not profilingJason Gross
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-04-23Merge PR #12130: [declare] [tactics] Move declare to `vernac`Pierre-Marie Pédrot
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-04-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias
2020-04-20Remove mod_constraints field of module bodyGaëtan Gilbert
2020-04-19Merge PR #12033: Let coqdoc be informed by coq about binding variables (incid...Lysxia
2020-04-17Deprecate “omega”Vincent Laporte
2020-04-16Merge PR #11861: [declare] [rewrite] Use high-level declare APIPierre-Marie Pédrot
2020-04-15Coqdoc: Exporting location and unique id for binding variables.Hugo Herbelin
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-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:38:43 +0000