aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
|
* 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
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Maxime Dénès2018-02-06
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6695: [toplevel] Refine start of interactive mode conditions.Gravatar Maxime Dénès2018-02-06
|\ \ \ \ \ \ \
| | | | | * | | Points to Flocq official repository.Gravatar Théo Zimmermann2018-02-05
| |_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | Following comment at https://github.com/coq/coq/pull/6596#issuecomment-358246528.
| | | | | * | Respect the transparent state of the current conversion on strong weak-head.Gravatar Pierre-Marie Pédrot2018-02-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes the previous patch in rare corner-cases where unification code was relying on both kernel conversion and specific transparent state.
| | | | * | | Add overlay for equations (nf_beta takes an env)Gravatar Gaëtan Gilbert2018-02-05
| | | | | | |
| | | * | | | [native_compute] Fix handling of evars in conversionGravatar Maxime Dénès2018-02-05
| | | | | | |
| | | * | | | [native_compute] Remove useless conversion to list in reification.Gravatar Maxime Dénès2018-02-05
| |_|/ / / / |/| | | | |
* | | | | | Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in ↵Gravatar Maxime Dénès2018-02-05
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | VernacDefinition
* \ \ \ \ \ \ Merge PR #6654: CI: Run coqchk on IrisGravatar Maxime Dénès2018-02-05
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6652: Allow vernacular controls before focus selectorGravatar Maxime Dénès2018-02-05
|\ \ \ \ \ \ \ \
| | | | | * | | | [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Emilio Jesus Gallego Arias2018-02-05
| | | | |/ / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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...
| | | | * / / / [toplevel] Refine start of interactive mode conditions.Gravatar Emilio Jesus Gallego Arias2018-02-05
| |_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * | | CClosure.unfold_projection: don't catch Not_found, assume env is okGravatar Gaëtan Gilbert2018-02-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We can do this after the parent commit (Reductionops.nf_* don't use empty env)
| | | | * | | Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
| | | | | | |
| | | | * | | checker: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This just shares the unfold_projection between Closure and Reduction.
| | | | * | | checker: remove unused per-constant reduction flags.Gravatar Gaëtan Gilbert2018-02-02
| | | | | | |
| | | | * | | kernel: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
| |_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | - use Redflags.red_projection - share unfold_projection between CClosure and Reduction
| | | | * | Use whd-all on rigid-flex conversion.Gravatar Pierre-Marie Pédrot2018-02-02
| |_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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`.
* | | | | Merge PR #6670: Delete duplicate lineGravatar Maxime Dénès2018-02-01
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant ↵Gravatar Maxime Dénès2018-02-01
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | error msg
* \ \ \ \ \ \ Merge PR #6672: [stm] Move options to a per-document record.Gravatar Maxime Dénès2018-02-01
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6660: [lib] Respect change of options under with/without_option.Gravatar Maxime Dénès2018-02-01
|\ \ \ \ \ \ \ \
| | | | | | | * | [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
| | | | | | | | |
| | | | | | | * | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
| |_|_|_|_|_|/ / |/| | | | | | |
| | | | | | * | CI: Run coqchk on IrisGravatar Ralf Jung2018-01-31
| | | | | | | |
| | | * | | | | Proofview: enter_one: add __LOC__ argument to get relevant error msgGravatar Enrico Tassi2018-01-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * | | | | | [stm] Move options to a per-document record.Gravatar Emilio Jesus Gallego Arias2018-01-31
| |/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | Merge PR #6601: Circle CI: fix cache selection.Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | menhir.
* \ \ \ \ \ \ \ \ Merge PR #6663: [toplevel] Refactor load path handling.Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | Delete duplicate lineGravatar Paul Steckler2018-01-30
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | |
| | | | | | * | | | | [lib] Respect change of options under with/without_option.Gravatar Emilio Jesus Gallego Arias2018-01-30
| |_|_|_|_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | * | | | | | Put default value for NJOBS in ci-common.Gravatar Gaëtan Gilbert2018-01-30
| | | | | | | | | |
| * | | | | | | | | Adding an overlay for Equations.Gravatar Pierre-Marie Pédrot2018-01-30
| | | | | | | | | |
* | | | | | | | | | Merge PR #6666: Fix reduction of primitive projections on coinductive ↵Gravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | records for cbv and native_compute
* \ \ \ \ \ \ \ \ \ \ Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6636: Stop running duplicate Travis jobs on pull requests.Gravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6605: Safer VM interfacesGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6644: Use travis_retry on apt-get updateGravatar Maxime Dénès2018-01-30
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 18:22:33 +0000