aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-14detype_case predicate is not optionalGaëtan Gilbert
2018-02-14Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)Maxime Dénès
2018-02-14Merge PR #6713: Fix #6677: Critical bug with VM and universesMaxime Dénès
2018-02-14adapt to Coq#6676Enrico Tassi
2018-02-14[coq] Adapt to coq/coq#6745Emilio Jesus Gallego Arias
Nothing remarkable.
2018-02-14[build] Fix VM dynamic linking prep in byte builds.Emilio Jesus Gallego Arias
We correctly set the path of `libcoqrun` in non-local builds. This bug was introduced by #6038. c.f. #6475 , #5992.
2018-02-13Fix issue with spurious timing test failuresJason Gross
When none of the numbers get over 100, the width of the table was different. See https://github.com/coq/coq/pull/6736#issuecomment-365386802
2018-02-13coqdev.el: wait for 'compile to touch compilation-error-regexp-alistGaëtan Gilbert
(and alist-alist)
2018-02-13Add CHANGES entry for #1047Tej Chajed
2018-02-13coqdev.el: fix "compilate"-command typoGaëtan Gilbert
2018-02-13coqdev.el: shell-quote-argument the directory for make -CGaëtan Gilbert
2018-02-13coqdev.el: stop using when-let for emacs<25 compatibility.Gaëtan Gilbert
2018-02-13Fixing an anomaly in the presence of "let-in" in the type of a record.Hugo Herbelin
Was raised by Jason on Gitter.
2018-02-13Merge PR #6693: [toplevel] Refactor command line argument handling.Maxime Dénès
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-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code.
2018-02-12Add notation {x & P} for sigTTej Chajed
Analogous to existing `{x | P}` notation for `sig`, where the type of `x` is inferred instead of specified.
2018-02-12Merge PR #6565: [Backport script] Check .mli files are not changed.Maxime Dénès
2018-02-12Tentative fix for #6520: camlcity.org unresponsive makes AppVeyor fail.Théo Zimmermann
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-12Add test case for #6677.Maxime 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-12Fix #6677: Critical bug with VM and universesMaxime Dénès
This bug was present since the first patch adding universe polymorphism handling in the VM (Coq 8.5). Note that unsoundness can probably be observed even without universe polymorphism.
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-11Merge anomaly-traces-parser.el into coqdev.el.Gaëtan Gilbert
2018-02-11coqdev.el: add installation instructions.Gaëtan Gilbert
2018-02-11dest_{prod,lam}: no Cast case (it's removed by whd)Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 09:47:32 +0000