aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | | Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking ↵Gravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | links (#6697)
* | | | | | | | | | | Merge PR #6738: CHANGES for universe varianceGravatar Maxime Dénès2018-02-13
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| | | | | | | | |_|_|/ | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | | | Merge PR #6565: [Backport script] Check .mli files are not changed.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #1082: Fixing Print for inductive types with let-in in parametersGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | * | | | | | | | | CHANGES for universe varianceGravatar Gaëtan Gilbert2018-02-12
| | | | | | | | | | | |
| | | | | | | | * | | | Add test case for #6677.Gravatar Maxime Dénès2018-02-12
| | | | | | | | | | | |
* | | | | | | | | | | | Merge PR #6262: [error] Replace msg_error by a proper exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / / / |/| | | | | | | | | | |
* | | | | | | | | | | | Merge PR #1047: Support universe instances on the literal TypeGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6128: Simplification: cumulativity information is variance ↵Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | information.
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6729: [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6418: More detailed error messages for Canonical Structure, #6398Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6139: Make list functions returning sumbools transparentGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6718: Fix redirection to stderr in lint-repository error message.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6708: Mention -quiet flag for FailGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6706: ci-common: guess CI_BRANCH for local buildsGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6674: Delay computation of lifts in the reduction machine.Gravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | * | | Fix #6677: Critical bug with VM and universesGravatar Maxime Dénès2018-02-12
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | * | | | | | | | | | | inferCumulativity: add comment to explain [if not is_arity].Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | Documentation for cumulative inductive variance.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | Print inductive cumulativity info in About.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | Universe instance printer: add optional variance argument.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | Use specialized function for inductive subtyping inference.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This ensures by construction that we never infer constraints outside the variance model.
| | | | | | | | | | | | | | | | | | | * Merge anomaly-traces-parser.el into coqdev.el.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | | | * coqdev.el: add installation instructions.Gravatar Gaëtan Gilbert2018-02-11
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | Inference of inductive subtyping does not need an evar map.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 |= *)
| | | | | | | | | * | | | | | | | | | | [get_cumulativity_constraints] allowing further code sharing.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | |
| | | | | | | | | * | | | | | | | | | | Factorize code for comparing maybe-cumulative inductives.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The part in Reduction should be semantics preserving, but Reductionops only tried cumulativity if equality fails. This is probably wrong so I changed it.
| | | | | | | | | * | | | | | | | | | | Fix typo in Univ.CumulativityInfoGravatar Gaëtan Gilbert2018-02-10
| |_|_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | | | [vernac] Fix outdated comment.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | | | [nit] Remove some unnecessary global `open Feedback`Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | * | | | [vernac] [minor] Move print effects to top-level caller.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | |_|_|_|/ / / / | | | | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | | * | | | | | | | [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | |/ / / / / / / / | | | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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].
| | | | | | | | * | | | | | | | | [nativecomp] Remove ad-hoc handling of Dynlink exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| |_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead, we properly register a printer for such exception and update the code.
| | | | | | | | | | | | | * | | [toplevel] Small refactoring of fatal_error functions.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | [toplevel] Refactor command line argument handling.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | | | |/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We mostly separate command line argument parsing from interpretation, some (minor) imperative actions are still done at argument parsing time. This tidies up the code quite a bit and allows to better follow the complicated command line handling code. To this effect, we group the key actions to be performed by the toplevel into a new record type. There is still room to improve.
| | | | | * | | | | | | / / / Fix redirection to stderr in lint-repository error message.Gravatar Gaëtan Gilbert2018-02-08
| |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | |
| | | | * | | | | | | | | | mention interactive mode for Fail messageGravatar Paul Steckler2018-02-07
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | | | | * | | [toplevel] Disable error resiliency in `-quick` mode.Gravatar Emilio Jesus Gallego Arias2018-02-07
| |_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #6707, indeed, the STM was treating some errors as recoverable thus `-quick` did succeed too often.
* | | | | | | | | | | | Merge PR #6657: Document the Fail commandGravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6685: Use whd-all on rigid-flex conversion.Gravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6610: Points to Flocq official repository.Gravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6686: Kernel/checker reduction cleanups around projection unfoldingGravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6673: Fix evar handling in native_compute conversionGravatar Maxime Dénès2018-02-07
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | | | | | ci-common: guess CI_BRANCH for local buildsGravatar Gaëtan Gilbert2018-02-07
| |_|_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | | |
| | | | | | | | | | | | | * | | Possible fix for issue #6697Gravatar Yannick Forster2018-02-07
| |_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | |
| | | | | | | | | * | | | | | More detailed error messages for Canonical Structure, #6398Gravatar Paul Steckler2018-02-06
| |_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Maxime Dénès2018-02-06
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 05:46:23 +0000