aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-10-22Merge PR #10899: Fixes #10894 regression: uconstr was not anymore typed in ↵Pierre-Marie Pédrot
the Ltac-substituted environment Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-22Merge PR #10886: test-suite/Makefile: work when manually involved for ↵Enrico Tassi
dune-compiled Coq Reviewed-by: gares
2019-10-22FSetEqProperties: do not use “omega”Vincent Laporte
2019-10-22OrderedTypeEx: do not use “omega”Vincent Laporte
2019-10-22Zpower: do not use “omega”Vincent Laporte
2019-10-22Lia: make explicit which “zify” is usedVincent Laporte
2019-10-22ZMicromega: do not use “omega”Vincent Laporte
2019-10-22Qround: do not use “omega”Vincent Laporte
2019-10-22Qreduction: do not use “omega”Vincent Laporte
2019-10-22QArith_base: do not use “omega”Vincent Laporte
2019-10-22FSets: do not use “omega”Vincent Laporte
2019-10-22Znumtheory: do not use “omega”Vincent Laporte
2019-10-22Zdiv: do not use “omega”Vincent Laporte
2019-10-22Zcomplements: do not use “omega”Vincent Laporte
2019-10-22Merge PR #10787: Fix #10779 (hnf normalisation of instance + reification of ↵Vincent Laporte
overloaded operators) Ack-by: maximedenes Reviewed-by: vbgl
2019-10-21chore: Enclose the […get_reflexive_proof_ssr…] call in a ↵Erik Martin-Dorel
try/with->assert false as suggested by @gares (the Not_found exc may be catched by coq/ssr otherwise).
2019-10-21docs(changelog): Address @gares' commentErik Martin-Dorel
& Put the changelog entry in the proper folder
2019-10-21Improvements of zifyFrédéric Besson
- Fix reification of overloaded operators (triggers convertibility checks with existing terms) - Zify instances need not be in hnf - Fix specification of bool operators - Add (limited) support for comparison fixes #10779
2019-10-21Merge PR #10857: Fix votour after the change of representation of opaques.Maxime Dénès
Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2019-10-21Adding changelogHugo Herbelin
2019-10-21Fixes #10894: uconstr was not anymore typed in the Ltac-substituted environment.Hugo Herbelin
More precisely: The equivalent in #7288 (4dab4fc) to the former call to ltac_interp_name_env was not done anymore when interpreting uconstr's.
2019-10-21Merge PR #10863: Minor side effect universe cleanupsPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
2019-10-21Merge PR #10891: Fix #9851: anomaly when unsolved evar in Add RingPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-10-19Don't abort in test for #6323.Gaëtan Gilbert
This lets the checker verify that we didn't produce nonsense.
2019-10-19universes_of_private: return set instead of list of setsGaëtan Gilbert
2019-10-18Merge PR #10914: Fix Locate printing regressionHugo Herbelin
Reviewed-by: herbelin
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ↵Gaëtan Gilbert
the kernel. Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares
2019-10-18Adding a test for votour.Pierre-Marie Pédrot
2019-10-18Merge PR #10919: factorize or_var_mapPierre-Marie Pédrot
Reviewed-by: ppedrot Reviewed-by: vbgl
2019-10-18Merge PR #10913: re-expose UState.demote_seff_univsPierre-Marie Pédrot
Ack-by: gares Reviewed-by: ppedrot
2019-10-18Merge PR #8228: (Partially) Revert "Make Environ.globals abstract."Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-10-18Merge PR #10895: Logic: Add equivalence between weak excluded-middle and ↵Pierre-Marie Pédrot
classical De Morgan's law Reviewed-by: ppedrot
2019-10-18factorize or_var_mapAlexandre Moine
2019-10-18Merge PR #10915: Fix link to `xml-protocol.md` in `dev/README.md`Théo Zimmermann
Reviewed-by: Zimmi48
2019-10-18Fix votour after the change of representation of opaques.Pierre-Marie Pédrot
2019-10-18Allow to pass Ltac1 values to Ltac2 quotations.Pierre-Marie Pédrot
This is the dual of #10344.
2019-10-17Fix link to `xml-protocol.md` in `dev/README.md`Michael D. Adams
2019-10-17Fix Locate printing regressionGuillaume Melquiond
Fixes #9428. (Again.) This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them. Corrects a 8.9.1 → 8.10.0 regression. (cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)
2019-10-16re-expose UState.demote_seff_univsGaëtan Gilbert
provide minimal functionality for https://github.com/mit-plv/rewriter plugin (declaring inductives as side effects, so there's no private constant to use with emit_side_effects)
2019-10-16Simplify future forcing in Declare.Pierre-Marie Pédrot
2019-10-16Ensure that side-effect declarations reaching the kernel are forced.Pierre-Marie Pédrot
2019-10-16Split the function used to declare side-effects from the standard one.Pierre-Marie Pédrot
This ensures that side-effect declarations come with their body, in prevision of the decoupling of the Safe_typign API for CEP 40.
2019-10-16Cleaning up the previous code by ensuring statically invariants on opaque ↵Pierre-Marie Pédrot
proofs. We return the typing context directly instead of hiding it into the opaque data, and we take advantage of this to remove a few assertions known to hold statically.
2019-10-16Make explicit the delayed computation of opaque bodies in Term_typing.Pierre-Marie Pédrot
We separate the Term_typing inference API into two functions, one to typecheck just the immediate part of an entry, and another one to check after the fact that a delayed term is indeed a correct proof for an opaque entry. This commit is mostly moving code around, this should be 1:1 semantically.
2019-10-16Merge PR #10885: Remove [in_section] arguments to Safe_typing functionsPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-16[engine] Remove UnivGen.global_of_constrVincent Laporte
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
Opening up a lambda should always lift the substitution attached to it.
2019-10-16Define sphinx replacements for \SProp \Type etcGaëtan Gilbert
2019-10-16Merge PR #10896: Assign ownership of the test-suite compat filesThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-15Merge PR #10854: Fix alphabetical ordering in contributors to 8.10.0.Clément Pit-Claudel
Ack-by: cpitclaudel Reviewed-by: jfehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 21:16:37 +0000