aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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[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
2020-03-19Fuck off ocamlformat.Pierre-Marie Pédrot
2020-03-19Reduce the scope of a call to pervasive equality in Coq_micromega.Pierre-Marie Pédrot
2020-03-19Use monomorphic comparison functions in Micromega.Vect.Pierre-Marie Pédrot
2020-03-19Dedicate type for monomials in Micromega.Vect.Pierre-Marie Pédrot
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
2020-03-13[funind] [cleanup] Remove unused function parametersEmilio Jesus Gallego Arias
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
2020-03-13Replacing catchable_exception by noncritical in try-with blocks.Hugo Herbelin
2020-03-11Merge PR #11754: [micromega] Add numerical compatibility layer.Frédéric Besson
2020-03-11Merge PR #11790: [lib] [ccalgo] Remove unused code / cleanupPierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:05:12 +0000