aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-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-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-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-16Merge PR #10885: Remove [in_section] arguments to Safe_typing functionsPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
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
2019-10-15Merge PR #10882: Document Gaëtan's new script to prefill a changelog entry.Clément Pit-Claudel
Ack-by: SkySkimmer Reviewed-by: cpitclaudel
2019-10-14Assign ownership of the test-suite compat filesJason Gross
I want to be notified when these are changed
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
Reviewed-by: JasonGross Reviewed-by: gares Ack-by: ppedrot
2019-10-14Merge PR #10852: Fix #10842: incorrect handling of unicode input before spacePierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-10-14Updating changelogHugo Herbelin
2019-10-14ClassicalFacts.v: Unifying format for bibliographical references.Hugo Herbelin
2019-10-14Weak excluded-middle: adding a reference.Hugo Herbelin
2019-10-14Logic: Add equivalence between weak excluded-middle and classical Morgan's lawHugo Herbelin
2019-10-14Fix #9851: anomaly when unsolved evar in Add RingGaëtan Gilbert
AFAICT there is no reason to use interp_open_constr I used Evd.from_ctx to keep passing evar maps around but maybe we should be passing ustates instead?
2019-10-14Remove obj_sec field of Nametab.obj_prefix record.Gaëtan Gilbert
There are no more users.
2019-10-14Use kernel info from Global for Lib.sections_{depth,are_opened}Gaëtan Gilbert
2019-10-14Remove [in_section] arguments to Safe_typing functionsGaëtan Gilbert
The information is already there. At some point we may want to clean up the Lib API to reduce redundancy wrt kernel functions like [sections_are_opened], but I'm not doing now as it would conflict with https://github.com/coq/coq/pull/10670
2019-10-14Merge PR #10887: fix rev_right_loop docEnrico Tassi
Reviewed-by: gares
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-14Merge PR #10889: Fix #10888: Context import behaviour in modtypePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-14Merge PR #10881: [make] separate generated gramlib ml files from mli files ↵Vincent Laporte
(fix #10864) Reviewed-by: SkySkimmer
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-10-13Fix #10888: Context import behaviour in modtypeGaëtan Gilbert
2019-10-13fix rev_right_loop docAntonio Nikishaev
2019-10-13Merge PR #10862: Simplify universe handling wrt side effects: rm ↵Pierre-Marie Pédrot
demote_seff_univs Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-13Merge PR #10670: ComAssumption cleanupPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:14:21 +0000