aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-12Merge PR #1082: Fixing Print for inductive types with let-in in parametersMaxime Dénès
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[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-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-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
2018-02-05[native_compute] Remove useless conversion to list in reification.Maxime Dénès
2018-02-05Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in ↵Maxime Dénès
VernacDefinition
2018-02-05Merge PR #6654: CI: Run coqchk on IrisMaxime Dénès
2018-02-05Merge PR #6652: Allow vernacular controls before focus selectorMaxime Dénès
2018-02-05[stm] [toplevel] Make loadpath a parameter of the document.Emilio Jesus Gallego Arias
We allow to provide a Coq load path at document creation time. This is natural as the document naming process is sensible to a particular load path, thus clarifying this API point. The changes are minimal, as #6663 did most of the work here. The only point of interest is that we have split the initial load path into two components: - a ML-only load path that is used to locate "plugable" toplevels. - the normal loadpath that includes `theories` and `user-contrib`, command line options, etc...
2018-02-05[toplevel] Refine start of interactive mode conditions.Emilio Jesus Gallego Arias
Refinement of the toplevel codepath requires to be more careful about the conditions for coqtop to be interactive. Fixes #6691. We also tweak the vio auxiliary function.
2018-02-04Delay computation of lifts in the reduction machine.Pierre-Marie Pédrot
This definitely qualifies as a micro-optimization, but it would not be performed by Flambda. Indeed, it is unsound in general w.r.t. OCaml semantics, as it involves a fixpoint and changes potential non-termination. In our case it doesn't matter semantically, but it is indeed observable on computation intensive developments like UniMath.
2018-02-02CClosure.unfold_projection: don't catch Not_found, assume env is okGaëtan Gilbert
We can do this after the parent commit (Reductionops.nf_* don't use empty env)
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2018-02-02checker: cleanup projection unfoldingGaëtan Gilbert
This just shares the unfold_projection between Closure and Reduction.
2018-02-02checker: remove unused per-constant reduction flags.Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 11:41:19 +0000