aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-11Merge PR #10850: chmod -x some filesGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-10-11Merge PR #10697: [vernac] Split vernacular translation and interpretation.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: gares
2019-10-11Merge PR #10844: Bump version number to 8.11.Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-10-10Merge PR #10817: Remove redundancy in section hypotheses of kernel entries.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-10-08Merge PR #10840: Release process: release notesThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-08Merge PR #10791: Replace custom timeout logic with new GitLab's per-job ↵Emilio Jesus Gallego Arias
timeout keyword. Reviewed-by: ejgallego
2019-10-08Merge PR #10770: [ci] Add mit-pdos/perennialEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-10-08Merge PR #10780: [CI/Azure/macOS] Update GTK3 to 3.24.11Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-10-07chmod -x some filesJason Gross
They probably don't need to be executable
2019-10-07Release process: release notesVincent Laporte
Explain into the release process how to prepare the release notes.
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
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-07[vernac] Split vernacular translation and interpretation.Emilio Jesus Gallego Arias
This allows UI clients to implement a different state management strategy with regards to proofs, and in particular to override `Vernacinterp.interp`. This is work in progress towards having a true `VtTactic` which shall not perform any state changes non-functionally, and actually removing the series of `assert false` due to meta-vernacs.
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-04Remove redundancy in section hypotheses of kernel entries.Pierre-Marie Pédrot
We only do it for entries and not declarations because the upper layers rely on the kernel being able to quickly tell that a definition is improperly used inside a section. Typically, tactics can mess with the named context and thus make the use of section definitions illegal. This cannot happen in the kernel but we cannot remove it due to the code dependency. Probably fixing a soundness bug reachable via ML code only. We were doing fancy things w.r.t. computation of the transitive closure of the the variables, in particular lack of proper sanitization of the kernel input.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:28:13 +0000