aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-02Cleanup tactic_option a bitGaëtan Gilbert
2020-04-02Merge pull request #11993 from olaure01/ollibs-wfnat-changelogAnton Trunov
[stdlib] Add changelog for PR #11335
2020-04-01Merge PR #9803: Adding more trigonometry in RealsHugo Herbelin
Ack-by: MSoegtropIMC Ack-by: Zimmi48 Ack-by: herbelin
2020-04-01Merge pull request #11946 from olaure01/ollibs-permutationAnton Trunov
[stdlib] Add complementary results about Permutation
2020-04-01Add changelog for PR #11249Olivier Laurent
2020-04-01Merge PR #10592: coqdoc: Add a new `details' environment for coqdocLysxia
Reviewed-by: Lysxia Reviewed-by: Zimmi48
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
- Added derivative for asin and acos - Added a few additional trigonometry lemmas - Added Lemmas for the derivative of a decreasing inverse function - Did some cleanup (move lemmas to the files where they belong)
2020-04-01- Addition to the Reals theory :thery
- minus: lemmas `Rminus_eq_0` and `Rmult_minus_distr_r` - sin : sin_inj - cos : cos_inj - sqrt : lemmas `pow2_sqrt` and `inv_sqrt` - atan : lemmas `tan_inj`, `atan_eq0`, `atan_tan` and `tan_atan` - asin : definition and some basic properties - acos : definition and some basic properties
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
Ack-by: SkySkimmer Reviewed-by: maximedenes
2020-04-01Merge PR #11873: python3 script does not need to import from the futureEmilio Jesus Gallego Arias
Reviewed-by: JasonGross
2020-04-01Merge PR #11945: Fix #11941: anomaly in equality schemesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-04-01Merge PR #11960: Docgram use new no update optionEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-01Merge PR #11971: [ci] Run bignums' testsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-01Merge pull request #11880 from Lysxia/iterAnton Trunov
NArith, PArith: Add facts about iter
2020-04-01[lib] Remove custom backtrace destroying finalizersEmilio Jesus Gallego Arias
in favor of the one in the OCaml standard library.
2020-03-31Merge PR #11933: Fix calling test suite makefile with a dune built coqEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-03-31Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit ↵Hugo Herbelin
arguments Ack-by: SkySkimmer Ack-by: gares Reviewed-by: 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
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares Reviewed-by: ppedrot
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
Co-authored-by: Jasper Hugunin <jasper@hugunin.net> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-31Merge PR #11684: Remove spurious anomalies in kernel reductionPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-31Merge PR #11823: [funind] [cleanup] Remove unused function parametersPierre-Marie Pédrot
Reviewed-by: Matafou Reviewed-by: ppedrot
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
As suggested by Gaëtan Gilbert.
2020-03-31[proof] [stm] Force `opaque` in `close_future_proof`Emilio Jesus Gallego Arias
Following an observation by Enrico Tassi, we remove the `opaque` parameter from `close_future_proof`, it should never be called with transparent constants. We will enforce this thru typing at the proof layer soon.
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
After the last refactoring commit, the entry_fn function is redundant and we can just get rid of it and get a more direct code.
2020-03-31[proof] Minor refactorings in Proof_globalEmilio Jesus Gallego Arias
We do some minor refactoring, removing one-use local definitions, and cleaning up the `EConstr.t -> Constr.t` path, what is going on with the use of unsafe it now becomes clear.
2020-03-31[proof] Split return_proof in partial and regular versions.Emilio Jesus Gallego Arias
This is a small refactoring as these two functions behave very differently and the invariants are quite different, in fact regular `return_proof` should not be exported but be part of close proof, but there is small use in the STM still.
2020-03-31[proof] Split delayed and regular proof closing functions, part IIEmilio Jesus Gallego Arias
We make the types of the delayed / non-delayed declaration path different, as the latter is just creating futures that are forced right away. TTBOMK the new code should behave identically w.r.t. old one, modulo the equation `Future.(force (from_val x)) = x`. There are some questions as what the code is doing, but in this PR I've opted to keep the code 100% faithful to the original one, unless I did a mistake.
2020-03-31[proof] Split delayed and regular proof closing functions, part IEmilio Jesus Gallego Arias
We split the `close_proof` into two variants, one for delayed proof, and one for the regular proof closing path, _à la_ interactive. This makes sense as the typing in both cases is different, even if we still haven't changed it. We strongly enforce the invariant (for now) that universe polymorphic proofs cannot be delayed using this API, as the STM expects. It introduces some minimal, non-interesting code duplication, which will go away in the next commits.
2020-03-31Merge PR #11818: [proof] Further consolidation of the regular declaration pathGaëtan Gilbert
Ack-by: Matafou Reviewed-by: SkySkimmer
2020-03-31Merge PR #11131: [ci] [gitlab] Add test-suite test for OCaml 4.10 and 4.11Théo Zimmermann
Ack-by: SkySkimmer Reviewed-by: Zimmi48
2020-03-31[ci] Run bignums' testsPierre Roux
2020-03-31Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the ↵Maxime Dénès
grammar. Reviewed-by: ejgallego Reviewed-by: maximedenes
2020-03-30[declare] [nit] Get `fix_exn` only in the case of an exception.Emilio Jesus Gallego Arias
Suggested by Gaëtan Gilbert.
2020-03-30[typeclasses] Use label for `fail_evar` parameter.Emilio Jesus Gallego Arias
This makes code a bit more clear.
2020-03-30[ci] [overlays] Adapt to declare API changes.Emilio Jesus Gallego Arias
- problem with metacoq overlay ; it expects to send a non-ground constant to the kernel, now it fails at prepare. Record Sigma (A : Type) (B : A -> Type) : Type := { fst : A ; snd : B fst }. Arguments fst {A B}. Arguments snd {A B}. Quote Recursively Definition foo := (fst, snd). There is a hack on the overlay, we need to discuss it a bit more.
2020-03-30[declare] Fuse prepare and declare for the non-interactive path.Emilio Jesus Gallego Arias
This will allow to share the definition metadata for example with obligations; a bit more work is needed to finally move the preparation of interactive proofs from Proof_global to `prepare_entry`.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 15:40:51 +0000