aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-07Bump version number to 8.11.Pierre-Marie Pédrot
2019-10-07Merge PR #9933: Add a few missing notes to the release doc.Vincent Laporte
Ack-by: ejgallego Reviewed-by: vbgl
2019-10-06Merge PR #10834: Fix #10831: minor issues in documentation of Function.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-10-06Merge PR #10833: 8.10.0 release notes.Vincent Laporte
Reviewed-by: vbgl
2019-10-06Fix #10831: minor issues in documentation of Function.Théo Zimmermann
2019-10-068.10.0 release notes.Théo Zimmermann
2019-10-05Merge PR #10763: Fix syntax of reduction tactics when listing qualid to ↵Vincent Laporte
reduce or not. Reviewed-by: jfehrle
2019-10-04Improve language.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2019-10-04Merge PR #9772: [Stdlib] OrderedType: do not pollute the “core” hint ↵Pierre-Marie Pédrot
database Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-10-04Merge PR #10798: Loosen restrictions on mixing universe mono/polymorphism in ↵Pierre-Marie Pédrot
sections Reviewed-by: ppedrot
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-10-04Merge PR #10806: Micromega tactics are no longer confused by primitive ↵Frédéric Besson
projections Reviewed-by: fajb
2019-10-03Merge PR #10765: Improved handling of micromega cachesPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot Ack-by: vbgl
2019-10-03fix 10765-micromega-caches.rstFrédéric Besson
2019-10-03Merge PR #10727: [library] Move `Declaremods` to `vernac/`Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: herbelin Reviewed-by: ppedrot
2019-10-03Improved handling of micromega cachesFrédéric Besson
- Specialised hash and equality functions. Avoid collisions in extreme scenarios. - Flags to disable the use of the caches. fixes #10772
2019-10-02Merge PR #10809: Postpone the computation of relative constraints in ↵Gaëtan Gilbert
universe unification Reviewed-by: SkySkimmer
2019-10-02Merge PR #10768: [ci] Update to OCaml 4.09.0, drop now useless "trunk" jobs.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-10-02Loosen restrictions on mixing universe mono/polymorphism in sectionsGaëtan Gilbert
We disallow adding univ constraints wich refer to polymorphic universes, and monomorphic constants and inductives when polymorphic universes or constraints are present. Every other combination is already correctly discharged by the kernel.
2019-10-02simplify branch in process_universe_constraintsGaëtan Gilbert
2019-10-02Merge PR #10805: Remove spurious uses of CoInductive in SSR prerequisite.Maxime Dénès
Reviewed-by: maximedenes
2019-10-02Postpone the computation of relative constraints in universe unification.Pierre-Marie Pédrot
Should be 1:1 equivalent to the previous code, this is semantics preserving factorization.
2019-10-01[Micromega] Use EConstr.eq_constr_universes_projVincent Laporte
2019-10-01Remove spurious uses of CoInductive in SSR prerequisite.Pierre-Marie Pédrot
2019-10-01Merge PR #10797: Implement discharging in kernelGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2019-09-29Merge PR #10673: [lemmas] Cleanup users of default proof information.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-09-28Remove the monomorphic universe libobject.Pierre-Marie Pédrot
No need to keep track of it this way now that this data is part of the kernel.
2019-09-26Move the declararation of delayed constraints out of add_constant_aux.Pierre-Marie Pédrot
This allows to remove the double declaration of monomorphic universes of discharged section constants. This also makes it much clearer that only the first declaration of a constant is allowed to declare delayed constraints. As a nice bonus, this simplifies the Opaqueproof API.
2019-09-26Implement section discharging inside kernel.Pierre-Marie Pédrot
This patch is minimalistic, insofar as it is only untying the dependency loop between Declare and Safe_typing. Nonetheless, it is already quite big, thus we will polish it afterwards.
2019-09-26Merge PR #10664: Putting sections libstack inside the kernelMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-25Clean up InferCumulativity after its move to the kernel.Pierre-Marie Pédrot
2019-09-25Move the Lib section data into the kernel.Pierre-Marie Pédrot
Due to the redundancy with some other declaration-specific data from the kernel, we also seize the opportunity to clean it up. Note also that discharging is still performed outside of the kernel for now.
2019-09-25Move cumulativity inference to the kernel.Pierre-Marie Pédrot
This is not quite pretty, but it is needed by the section mechanism to rebuild an inductive when closing a section. Hopefully this can be moved back at some point.
2019-09-25Stub code for handling sections in kernel.Pierre-Marie Pédrot
For now we only keep a count of the number of open sections, discriminating between polymorphic and monomorphic ones.
2019-09-25Refine the API to declare section-local universes.Pierre-Marie Pédrot
The section local universes are undoubtedly ordered, but the API was requiring an unordered ContextSet. We also move the naming one level up. Unfortunately, some callers are currently defining the same polymorphic universes in a section several times, notably the "Variable" command. I had to hack around this behaviour.
2019-09-25Merge PR #10713: Define morphisms of real numbers and accelerate Cauchy realsHugo Herbelin
Reviewed-by: herbelin
2019-09-25Merge PR #10784: Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-09-25Merge PR #10781: Fixes #10778 (fresh was not updated after renaming of ↵Pierre-Marie Pédrot
intropattern entry in #10239) Reviewed-by: ppedrot
2019-09-24Merge PR #10774: Make `zify` does work for `Z.to_N`Frédéric Besson
Reviewed-by: Zimmi48 Reviewed-by: fajb
2019-09-24Merge PR #10699: [gitlab/ci] Prevent Corn from running if Bignums has failed.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-09-24Merge PR #10758: Fix #10757: Program Fixpoint uses "exists" for telescopesMatthieu Sozeau
Reviewed-by: mattam82
2019-09-24Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kindGaëtan Gilbert
2019-09-24Make `zify` does work for `Z.to_N`Kazuhiko Sakaguchi
2019-09-23Fixes #10778 (fresh was not updated after renaming of intropattern entry in ↵Hugo Herbelin
#10239). The bug was introduced in #10239 which seems to have actually remained half-done: "wit_intropattern" and "wit_simple_intropattern" did not share the same representation of values (val_tag) but the code was assuming (especially the code for "fresh") that this was shared. We fix it by sharing the internal representation (`dyn` field in Tacarg.make0) as suggested by @ppedrot in the discussion of #10239 (this allows also to simplify Taccoerce.is_intro_pattern).
2019-09-23Merge PR #10776: Fix #10413 (CI failure on tags).Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-09-23Merge PR #10777: Mark SF as allow failure until it gets fixed.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-09-23Mark SF as allow failure until it gets fixed.Théo Zimmermann
Failing CI is BAD. #10476 should not have been merged without a solution for SF being found, or the test being marked temporarily as allow failure.
2019-09-23Fix #10413 (CI failure on tags).Théo Zimmermann
On tags, the pkg:nix:deploy:channel job was run even though the required pkg:nix:deploy was not. We repeat the same conditions regarding refs as in pkg:nix:deploy. Cf. GitLab's doc on the meaning of several only conditions: https://docs.gitlab.com/ee/ci/yaml/README.html#onlyexcept-advanced
2019-09-20[ci] Remove OCaml "trunk" CI jobs.Emilio Jesus Gallego Arias
It will take non-trivial effort to make Coq work with OCaml >= 4.10.0.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 10:48:24 +0000