aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-03-31[proof] Improve comment and argument name.Emilio Jesus Gallego Arias
2020-03-31[proof] [stm] Force `opaque` in `close_future_proof`Emilio Jesus Gallego Arias
2020-03-31[proof] Remove unused parameter in the delayed save path.Emilio Jesus Gallego Arias
2020-03-31[proof] Fixme on unused return type.Emilio Jesus Gallego Arias
2020-03-31[proof] Remove internal wrapper in Proof_globalEmilio Jesus Gallego Arias
2020-03-31[proof] Minor refactorings in Proof_globalEmilio Jesus Gallego Arias
2020-03-31[proof] Split return_proof in partial and regular versions.Emilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
2020-03-31[proof] Split delayed and regular proof closing functions, part IEmilio Jesus Gallego Arias
2020-03-31Merge PR #11818: [proof] Further consolidation of the regular declaration pathGaëtan Gilbert
2020-03-31Merge PR #11131: [ci] [gitlab] Add test-suite test for OCaml 4.10 and 4.11Théo Zimmermann
2020-03-31[ci] Run bignums' testsPierre Roux
2020-03-31Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the gr...Maxime Dénès
2020-03-30[declare] [nit] Get `fix_exn` only in the case of an exception.Emilio Jesus Gallego Arias
2020-03-30[typeclasses] Use label for `fail_evar` parameter.Emilio Jesus Gallego Arias
2020-03-30[ci] [overlays] Adapt to declare API changes.Emilio Jesus Gallego Arias
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 18:04:54 +0000