aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-04-01Merge pull request #11946 from olaure01/ollibs-permutationAnton Trunov
2020-04-01Merge PR #10592: coqdoc: Add a new `details' environment for coqdocLysxia
2020-04-01Add complementary results about PermutationOlivier Laurent
2020-04-01Merge PR #11306: Centralize the flag handling native compilation.Maxime Dénès
2020-04-01Merge PR #11873: python3 script does not need to import from the futureEmilio Jesus Gallego Arias
2020-04-01Merge PR #11945: Fix #11941: anomaly in equality schemesEmilio Jesus Gallego Arias
2020-04-01Merge PR #11960: Docgram use new no update optionEmilio Jesus Gallego Arias
2020-04-01Merge PR #11971: [ci] Run bignums' testsEmilio Jesus Gallego Arias
2020-04-01Merge pull request #11880 from Lysxia/iterAnton Trunov
2020-03-31Merge PR #11933: Fix calling test suite makefile with a dune built coqEmilio Jesus Gallego Arias
2020-03-31Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit ...Hugo Herbelin
2020-03-31NArith, PArith: Add facts about iterLysxia
2020-03-31Merge PR #11915: [proof] Split delayed and regular proof closing functionsPierre-Marie Pédrot
2020-03-31Merge PR #11889: Fix a spelling mistake in the code: s/magicaly/magically/Enrico Tassi
2020-03-31Include review suggestionsGaëtan Gilbert
2020-03-31Try only using TC for conversion in cominductive (not great but let's see)Gaëtan Gilbert
2020-03-31Remove check_hidden_implicit_parameters (not needed anymore)Gaëtan Gilbert
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
2020-03-31Merge PR #11684: Remove spurious anomalies in kernel reductionPierre-Marie Pédrot
2020-03-31Merge PR #11823: [funind] [cleanup] Remove unused function parametersPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 18:27:42 +0000