| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2018-02-05 | [native_compute] Remove useless conversion to list in reification. | Maxime Dénès | |
| 2018-02-05 | Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in ↵ | Maxime Dénès | |
| VernacDefinition | |||
| 2018-02-05 | Merge PR #6654: CI: Run coqchk on Iris | Maxime Dénès | |
| 2018-02-05 | Merge PR #6652: Allow vernacular controls before focus selector | Maxime 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-04 | Delay 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-02 | CClosure.unfold_projection: don't catch Not_found, assume env is ok | Gaëtan Gilbert | |
| We can do this after the parent commit (Reductionops.nf_* don't use empty env) | |||
| 2018-02-02 | Reductionops.nf_* now take an environment. | Gaëtan Gilbert | |
| 2018-02-02 | checker: cleanup projection unfolding | Gaëtan Gilbert | |
| This just shares the unfold_projection between Closure and Reduction. | |||
| 2018-02-02 | checker: remove unused per-constant reduction flags. | Gaëtan Gilbert | |
| 2018-02-02 | kernel: cleanup projection unfolding | Gaëtan Gilbert | |
| - use Redflags.red_projection - share unfold_projection between CClosure and Reduction | |||
| 2018-02-02 | Use whd-all on rigid-flex conversion. | Pierre-Marie Pédrot | |
| This heuristic is justified by the fact that during a conversion check between a flexible and a rigid term, the flexible one is eventually going to be fully weak-head normalized. So in this case instead of performing many small reduction steps on the flexible term, we perform full weak-head reduction, including delta. It is slightly more efficient in actual developments, and it fixes a corner case encountered by Jason Gross. Fixes #6667: Kernel conversion is much, much slower than `Eval lazy`. | |||
| 2018-02-01 | Merge PR #6670: Delete duplicate line | Maxime Dénès | |
| 2018-02-01 | Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant ↵ | Maxime Dénès | |
| error msg | |||
| 2018-02-01 | Merge PR #6672: [stm] Move options to a per-document record. | Maxime Dénès | |
| 2018-02-01 | Merge PR #6660: [lib] Respect change of options under with/without_option. | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |