aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants.
2020-04-06Merge PR #11955: Use the kernel machine in whd_betaiota_deltazeta_for_iota_stateMatthieu Sozeau
Reviewed-by: SkySkimmer Reviewed-by: mattam82
2020-04-05Merge PR #12025: Fixes #11194 (Canonical/Coercion not located for coqdoc)Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-05Fixes #11194 (Canonical/Coercion not located for coqdoc).Hugo Herbelin
The location was missing in the parser.
2020-04-03Fix the test for bug #4544.Pierre-Marie Pédrot
It seems that this PR is making the rewrite much, much faster.
2020-04-03Be cleverer and do not hopelessly rezip a term when not needed.Pierre-Marie Pédrot
A quick analysis showed that most of the calls to whd do not lead to a term which further triggers reduction, so there is no point in refolding a potentiall huge term for no reason.
2020-04-03Use the kernel machine in whd_betaiota_deltazeta_for_iota_state.Pierre-Marie Pédrot
There is no point in using the exaggerately inefficient Reductionops machine. We need to be call-by-name to preserve the shape of the reduced terms, as call-by-need would introduce sharing and thus at-distance effects in term refolding. Yet, the Reductionops machine is worse than that, since it performs substitutions eagerly, leading to a catastrophical performance profile. Instead, we use the kernel reduction in by-name mode to replace the Reductionops machine in whd_betaiota_deltazeta_for_iota_state with all flags on. Since the kernel is using explicit substitutions, this is algorithmically more efficient. Apart from minor differences, this should produce the same normal form. As showed by the benchmarks, this is a critical change for the odd-order proofs. Ideally, we should use delayed substitutions in the Reductionops machine as well for great profit, but due to code entanglement this is a much less self-contained change.
2020-04-03Merge PR #12007: Fix CoRN & Flocq CI scripts.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-03Fix Flocq CI script.Théo Zimmermann
autogen.sh was removed in https://gitlab.inria.fr/flocq/flocq/-/commit/d679d3770aea2ff8608c77096158653837798124
2020-04-03Merge PR #11664: Encoding string list as a string with application to the ↵Emilio Jesus Gallego Arias
parsing of coqtop arguments in coqide Reviewed-by: ejgallego
2020-04-03Merge PR #11895: Remove Chapter command.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-03Merge PR #11914: Start the split of the Gallina Extensions chapter.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-04-03Split four sections out of the Gallina extensions chapter.Théo Zimmermann
This octopus merge is meant to preserve the commit history / blame of all the parts.
2020-04-03Move section in records in appropriate location (inside core).Théo Zimmermann
2020-04-03Move section on sections in appropriate location (inside core).Théo Zimmermann
2020-04-03Move section on funind in appropriate location (inside libraries).Théo Zimmermann
2020-04-03Move section on implicit arguments in appropriate location (inside extensions).Théo Zimmermann
2020-04-03Extract section on implicit arguments from Gallina extensions.Théo Zimmermann
2020-04-03Extract section on funind from Gallina extensions.Théo Zimmermann
2020-04-03Remove sections on records, sections, funind and implicit arguments from ↵Théo Zimmermann
gallina-ext chapter.
2020-04-03Extract section on sections from Gallina extensions.Théo Zimmermann
2020-04-03Extract section on records from Gallina extensions.Théo Zimmermann
2020-04-03Merge PR #12009: Adding changelog for 8.11.1.Théo Zimmermann
Reviewed-by: Zimmi48
2020-04-03Fix CoRN CI script.Théo Zimmermann
Auto-generated files like the Makefile have recently been removed from the sources (cf. coq-community/corn#88). Calling ./configure.sh is now required.
2020-04-03Adding changelog for 8.11.1.Pierre-Marie Pédrot
2020-04-03Merge PR #11996: [stdlib] Add changelog for PR #11249Anton Trunov
Reviewed-by: anton-trunov
2020-04-02Merge PR #11869: Add an index for attributes.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-04-02Merge PR #12002: Cleanup tactic_option a bitPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-02Remove Chapter command.Théo Zimmermann
This was an undocumented equivalent of the Section command.
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:05:45 +0000