aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-13Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.Maxime Dénès
2018-02-13Merge PR #6711: [toplevel] Disable error resiliency in `-quick` mode.Maxime Dénès
2018-02-13Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking ↵Maxime Dénès
links (#6697)
2018-02-13Merge PR #6738: CHANGES for universe varianceMaxime Dénès
2018-02-12Merge PR #6565: [Backport script] Check .mli files are not changed.Maxime Dénès
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
2018-02-12CHANGES for universe varianceGaëtan Gilbert
2018-02-12Merge PR #6262: [error] Replace msg_error by a proper exception.Maxime Dénès
2018-02-12Merge PR #1047: Support universe instances on the literal TypeMaxime Dénès
2018-02-12Merge PR #6128: Simplification: cumulativity information is variance ↵Maxime Dénès
information.
2018-02-12Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.Maxime Dénès
2018-02-12Merge PR #6418: More detailed error messages for Canonical Structure, #6398Maxime Dénès
2018-02-12Merge PR #6139: Make list functions returning sumbools transparentMaxime Dénès
2018-02-12Merge PR #6718: Fix redirection to stderr in lint-repository error message.Maxime Dénès
2018-02-12Merge PR #6708: Mention -quiet flag for FailMaxime Dénès
2018-02-12Merge PR #6706: ci-common: guess CI_BRANCH for local buildsMaxime Dénès
2018-02-12Merge PR #6651: Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-02-12Merge PR #6674: Delay computation of lifts in the reduction machine.Maxime Dénès
2018-02-11inferCumulativity: add comment to explain [if not is_arity].Gaëtan Gilbert
2018-02-11Documentation for cumulative inductive variance.Gaëtan Gilbert
2018-02-11Print inductive cumulativity info in About.Gaëtan Gilbert
2018-02-11Universe instance printer: add optional variance argument.Gaëtan Gilbert
2018-02-11Use specialized function for inductive subtyping inference.Gaëtan Gilbert
This ensures by construction that we never infer constraints outside the variance model.
2018-02-10Inference of inductive subtyping does not need an evar map.Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
2018-02-10[get_cumulativity_constraints] allowing further code sharing.Gaëtan Gilbert
2018-02-10Factorize code for comparing maybe-cumulative inductives.Gaëtan Gilbert
The part in Reduction should be semantics preserving, but Reductionops only tried cumulativity if equality fails. This is probably wrong so I changed it.
2018-02-10Fix typo in Univ.CumulativityInfoGaëtan Gilbert
2018-02-09[vernac] Fix outdated comment.Emilio Jesus Gallego Arias
2018-02-09[nit] Remove some unnecessary global `open Feedback`Emilio Jesus Gallego Arias
2018-02-09[vernac] [minor] Move print effects to top-level caller.Emilio Jesus Gallego Arias
We remove many individual calls to `msg_notice` in the print vernacular dispatcher in favor of a single, top-level calls. This is a minor refactoring but will help in handling `Print Foo` more uniformly.
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now].
2018-02-09[nativecomp] Remove ad-hoc handling of Dynlink exception.Emilio Jesus Gallego Arias
Instead, we properly register a printer for such exception and update the code.
2018-02-08Fix redirection to stderr in lint-repository error message.Gaëtan Gilbert
2018-02-07mention interactive mode for Fail messagePaul Steckler
2018-02-07[toplevel] Disable error resiliency in `-quick` mode.Emilio Jesus Gallego Arias
Fixes #6707, indeed, the STM was treating some errors as recoverable thus `-quick` did succeed too often.
2018-02-07Merge PR #6657: Document the Fail commandMaxime Dénès
2018-02-07Merge PR #6685: Use whd-all on rigid-flex conversion.Maxime Dénès
2018-02-07Merge PR #6610: Points to Flocq official repository.Maxime Dénès
2018-02-07Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingMaxime Dénès
2018-02-07Merge PR #6673: Fix evar handling in native_compute conversionMaxime Dénès
2018-02-07ci-common: guess CI_BRANCH for local buildsGaëtan Gilbert
2018-02-07Possible fix for issue #6697Yannick Forster
2018-02-06More detailed error messages for Canonical Structure, #6398Paul Steckler
2018-02-06Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Maxime Dénès
2018-02-06Merge PR #6695: [toplevel] Refine start of interactive mode conditions.Maxime Dénès
2018-02-05Points to Flocq official repository.Théo Zimmermann
Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528.
2018-02-05Respect the transparent state of the current conversion on strong weak-head.Pierre-Marie Pédrot
This fixes the previous patch in rare corner-cases where unification code was relying on both kernel conversion and specific transparent state.
2018-02-05Add overlay for equations (nf_beta takes an env)Gaëtan Gilbert
2018-02-05[native_compute] Fix handling of evars in conversionMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-19 02:45:08 +0000