| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-12 | Merge PR #6706: ci-common: guess CI_BRANCH for local builds | Maxime Dénès | |
| 2018-02-12 | Merge PR #6651: Use r.(p) syntax to print primitive projections. | Maxime Dénès | |
| 2018-02-12 | Merge PR #6674: Delay computation of lifts in the reduction machine. | Maxime Dénès | |
| 2018-02-12 | Fix #6677: Critical bug with VM and universes | Maxime 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-11 | inferCumulativity: add comment to explain [if not is_arity]. | Gaëtan Gilbert | |
| 2018-02-11 | Documentation for cumulative inductive variance. | Gaëtan Gilbert | |
| 2018-02-11 | Print inductive cumulativity info in About. | Gaëtan Gilbert | |
| 2018-02-11 | Universe instance printer: add optional variance argument. | Gaëtan Gilbert | |
| 2018-02-11 | Use specialized function for inductive subtyping inference. | Gaëtan Gilbert | |
| This ensures by construction that we never infer constraints outside the variance model. | |||
| 2018-02-11 | Merge anomaly-traces-parser.el into coqdev.el. | Gaëtan Gilbert | |
| 2018-02-11 | coqdev.el: add installation instructions. | Gaëtan Gilbert | |
| 2018-02-11 | dest_{prod,lam}: no Cast case (it's removed by whd) | Gaëtan Gilbert | |
| 2018-02-10 | Inference of inductive subtyping does not need an evar map. | Gaëtan Gilbert | |
| 2018-02-10 | Simplification: 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-10 | Factorize 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-10 | Fix typo in Univ.CumulativityInfo | Gaë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-09 | [toplevel] Small refactoring of fatal_error functions. | Emilio Jesus Gallego Arias | |
| 2018-02-09 | [toplevel] Refactor command line argument handling. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2018-02-08 | Fix redirection to stderr in lint-repository error message. | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: nicer messages | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: fail gracefully if fixing whitespace removes all changes | Gaëtan Gilbert | |
| 2018-02-08 | pre-commit: add files after fixing ending newlines. | Gaëtan Gilbert | |
| 2018-02-08 | Document configure setting up pre-commit hook in CONTRIBUTING.md | Gaëtan Gilbert | |
| 2018-02-08 | Have the pre-commit hook also fix end-of-file nl | Jason Gross | |
| 2018-02-08 | Auto-create .git/hooks/pre-commit on ./configure | Jason Gross | |
| The hook created checks to see if dev/tools/pre-commit exists, and, if so, runs it. This way, we don't have to do any fancy logic to update the git pre-commit hook. The configure script never overwrites an existing precommit hook, so users can disable it by creating an empty pre-commit hook. The check for existence is so that if users check out an old version of Coq, attempting to commit won't give an error about non-existent files. | |||
| 2018-02-08 | pre-commit hook: fix whitespace error detection | Gaëtan Gilbert | |
| --quiet implies --exit-code | |||
| 2018-02-08 | Mention linter and pre-commit hook in CONTRIBUTING.md. | Gaëtan Gilbert | |
| 2018-02-08 | A pre-commit hook to magically fix whitespace issues. | Gaëtan Gilbert | |
| 2018-02-07 | mention interactive mode for Fail message | Paul 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-07 | Merge PR #6657: Document the Fail command | Maxime Dénès | |
| 2018-02-07 | Merge PR #6685: Use whd-all on rigid-flex conversion. | Maxime Dénès | |
| 2018-02-07 | Merge PR #6610: Points to Flocq official repository. | Maxime Dénès | |
| 2018-02-07 | Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding | Maxime Dénès | |
| 2018-02-07 | Merge PR #6673: Fix evar handling in native_compute conversion | Maxime Dénès | |
| 2018-02-07 | ci-common: guess CI_BRANCH for local builds | Gaëtan Gilbert | |
| 2018-02-07 | Possible fix for issue #6697 | Yannick Forster | |
| 2018-02-06 | More detailed error messages for Canonical Structure, #6398 | Paul Steckler | |
| 2018-02-06 | Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document. | Maxime Dénès | |
| 2018-02-06 | Merge PR #6695: [toplevel] Refine start of interactive mode conditions. | Maxime Dénès | |
| 2018-02-05 | Points to Flocq official repository. | Théo Zimmermann | |
| Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528. | |||
| 2018-02-05 | Respect 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-05 | Add overlay for equations (nf_beta takes an env) | Gaëtan Gilbert | |
| 2018-02-05 | [native_compute] Fix handling of evars in conversion | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |