aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-04-02Cleanup tactic_option a bitGaëtan Gilbert
2020-04-02Merge pull request #11993 from olaure01/ollibs-wfnat-changelogAnton Trunov
2020-04-01Merge PR #9803: Adding more trigonometry in RealsHugo Herbelin
2020-04-01Merge pull request #11946 from olaure01/ollibs-permutationAnton Trunov
2020-04-01Add changelog for PR #11249Olivier Laurent
2020-04-01Merge PR #10592: coqdoc: Add a new `details' environment for coqdocLysxia
2020-04-01Add changelog for PR #11335Olivier Laurent
2020-04-01- Adjusted definitions and lemmas for asin and acos to what has been discussedMichael Soegtrop
2020-04-01- Addition to the Reals theory :thery
2020-04-01Add complementary results about PermutationOlivier Laurent
2020-04-01add tests for notations with sigma typesOlivier Laurent
2020-04-01[micromega] use Coqlib.lib_ref to get Coq constants.Frédéric Besson
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-04-01[lib] Remove custom backtrace destroying finalizersEmilio Jesus Gallego Arias
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[nit] [plugin_tuto] Remove empty function and use new API directlyEmilio Jesus Gallego Arias
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] 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 21:05:31 +0000