| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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-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-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-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 | |
| 2018-01-30 | [lib] Respect change of options under with/without_option. | Emilio Jesus Gallego Arias | |
| The old semantics of `with/without_option` allowed the called function to modify the value of the option. This is an issue mainly with the `silently/verbose` combinators, as `Set Silent` can be executed under one of them and thus the modification will be lost in the updated code introduced in a554519874c15d0a790082e5f15f3dc2419c6c38 IMHO these kind of semantics are quite messy but we have to preserve them in order for the `Silent` system to work. In fact, note that in the previous code, `with_options` was not consistent with `with_option` [maybe that got me confused?] Ideally we could restore the saner semantics once we clean up the `Silent` system [that is, we remove the flag altogether], but that'll have to wait. Fixes #6645. | |||
| 2018-01-30 | Put default value for NJOBS in ci-common. | Gaëtan Gilbert | |
| 2018-01-30 | Adding an overlay for Equations. | Pierre-Marie Pédrot | |
| 2018-01-30 | Merge PR #6666: Fix reduction of primitive projections on coinductive ↵ | Maxime Dénès | |
| records for cbv and native_compute | |||
| 2018-01-30 | Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projections | Maxime Dénès | |
| 2018-01-30 | Merge PR #6636: Stop running duplicate Travis jobs on pull requests. | Maxime Dénès | |
| 2018-01-30 | Merge PR #6605: Safer VM interfaces | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |