| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-02-12 | Merge PR #6418: More detailed error messages for Canonical Structure, #6398 | Maxime Dénès | |
| 2018-02-12 | Merge PR #6139: Make list functions returning sumbools transparent | Maxime Dénès | |
| 2018-02-12 | Merge PR #6718: Fix redirection to stderr in lint-repository error message. | Maxime Dénès | |
| 2018-02-12 | Merge PR #6708: Mention -quiet flag for Fail | Maxime Dénès | |
| 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-08 | Fix redirection to stderr in lint-repository error message. | Gaëtan Gilbert | |
| 2018-02-07 | mention interactive mode for Fail message | Paul Steckler | |
| 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-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 | |
| 2018-02-01 | [vernac] Mutual theorems (VernacStartTheoremProof) always have names | Vincent Laporte | |
| 2018-02-01 | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition | Vincent Laporte | |
| 2018-01-31 | CI: Run coqchk on Iris | Ralf Jung | |
| 2018-01-31 | Proofview: enter_one: add __LOC__ argument to get relevant error msg | Enrico Tassi | |
| The type discipline of the tactic monad does not distinguish between mono-goal and multi-goal tactics. Unfortunately enter_one "asserts false" if called on 0 or > 1 goals. The __LOC__:string argument can be used to make the error message more helpful (since the backtrace is pointless inside the monad). The intended usage is "Goal.enter_one ~__LOC__ (fun gl -> ..". The __LOC__ variable is filled in by the OCaml compiler with the current file name and line number. | |||
| 2018-01-31 | [stm] Move options to a per-document record. | Emilio Jesus Gallego Arias | |
| We gather (almost) all the STM options in a record, now set at document creation time. This is refactoring is convenient for some other ongoing functionalization work. | |||
| 2018-01-31 | Merge PR #6601: Circle CI: fix cache selection. | Maxime Dénès | |
| 2018-01-31 | Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵ | Maxime Dénès | |
| menhir. | |||
| 2018-01-31 | Merge PR #6663: [toplevel] Refactor load path handling. | Maxime Dénès | |
| 2018-01-31 | Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees" | Maxime Dénès | |
| 2018-01-31 | Merge PR #6535: Cleanup name-binding structure for fresh evar name generation. | Maxime Dénès | |
| 2018-01-30 | Delete duplicate line | Paul Steckler | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |