aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-30[lemmas] Minor tweak to Equations API.Emilio Jesus Gallego Arias
2020-03-30[program] Use common type for fixpoint declarations.Emilio Jesus Gallego Arias
2020-03-30[doc] [obligations] Some notes about `Program` implementationEmilio Jesus Gallego Arias
2020-03-30[classes] Declare obligation implicits using standard API.Emilio Jesus Gallego Arias
2020-03-30[declareDef] More consistent handling of universe bindersEmilio Jesus Gallego Arias
2020-03-30[declareObl] Remove hack w.r.t. to universe normalization.Emilio Jesus Gallego Arias
2020-03-30[obligations] Remove unnecessary ctx variableEmilio Jesus Gallego Arias
2020-03-30[declare] Make the type of closed entries opaque.Emilio Jesus Gallego Arias
2020-03-30[declareDef] Cleanup of allow_evars and check_evarsEmilio Jesus Gallego Arias
2020-03-30[declare] [obligations] Refactor preparation of obligation entryEmilio Jesus Gallego Arias
2020-03-30[ComDefinition] Split program from regular declarationsEmilio Jesus Gallego Arias
2020-03-30[lemmas] Cleanup in handling of mutual definitionsEmilio Jesus Gallego Arias
2020-03-30[lemmas] Remove workaround for non-uniform mutual bodyEmilio Jesus Gallego Arias
2020-03-30[comFixpoint] Minor cleanups in type declarations.Emilio Jesus Gallego Arias
2020-03-30[lemmas] [internal] Reify handling of mutual assumptionsEmilio Jesus Gallego Arias
2020-03-30[proof] Miscellaneous cleanup on proof info handlingEmilio Jesus Gallego Arias
2020-03-30[lemma] Remove special case for first constant in mutual definition save path.Emilio Jesus Gallego Arias
2020-03-31Merge PR #11647: [rfc] Consolidation of parsing interfacesPierre-Marie Pédrot
2020-03-30Merge PR #11725: Cleanup stdlib reals.Hugo Herbelin
2020-03-30Merge PR #11969: ocamlformat: use whitelist instead of blacklistEmilio Jesus Gallego Arias
2020-03-30Merge PR #11965: Partial revert of #11817.Emilio Jesus Gallego Arias
2020-03-30Merge PR #11968: Fix commit hook when there are no changes (eg amend message)Emilio Jesus Gallego Arias
2020-03-30ocamlformat: use whitelist instead of blacklistGaëtan Gilbert
2020-03-30Fix commit hook when there are no changes (eg amend message)Gaëtan Gilbert
2020-03-30Missing apartness notationsVincent Semeria
2020-03-30new sig notations and spaces addedOlivier Laurent
2020-03-30Partial revert of #11817.Pierre-Marie Pédrot
2020-03-30Merge PR #11921: Remove some cruft from Reductionops API.Gaëtan Gilbert
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
2020-03-30Merge PR #11951: Remove a useless reversed variant in Vars.Gaëtan Gilbert
2020-03-30[dune] [docgram] Remove bash hack thanks to new option -no-update.Théo Zimmermann
2020-03-30Merge PR #11958: Add -no-update command line option to doc_grammar for DuneThéo Zimmermann
2020-03-30Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”Maxime Dénès
2020-03-30Merge PR #11874: Auto-format micromega files in pre-commit hook.Emilio Jesus Gallego Arias
2020-03-29[ci] [gitlab] Bump to edge to OCaml 4.10, add test-suite for OCaml 4.11Emilio Jesus Gallego Arias
2020-03-29[configure] Disable warning 67 which seems 100% bogusEmilio Jesus Gallego Arias
2020-03-29Update 11909-fix-≡-level.rstJason Gross
2020-03-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
2020-03-29Merge PR #11938: Support for updating orderedGrammar with Dune.Emilio Jesus Gallego Arias
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
2020-03-29Merge PR #11944: Remove SearchAbout command, deprecated in 8.5Théo Zimmermann
2020-03-28Merge PR #11950: Document change of behavior of Fail in 8.11.Clément Pit-Claudel
2020-03-28Remove a useless reversed variant in Vars.Pierre-Marie Pédrot
2020-03-28Remove some cruft from Reductionops API.Pierre-Marie Pédrot
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Document change of behavior of Fail in 8.11.Théo Zimmermann
2020-03-28coqdoc: Add (* begin details *) and (* end details *)Thomas Letan
2020-03-28Update fullGrammar and orderedGrammar following #11877.Théo Zimmermann
2020-03-28New target check-gram to check if fullGrammar and orderedGrammar are up-to-date.Théo Zimmermann
2020-03-28Fix #11941: anomaly in equality schemesGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 21:11:43 +0000