aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-07Merge PR #6673: Fix evar handling in native_compute conversionMaxime Dénès
2018-02-06Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.Maxime Dénès
2018-02-06Merge PR #6695: [toplevel] Refine start of interactive mode conditions.Maxime Dénès
2018-02-05[native_compute] Fix handling of evars in conversionMaxime Dénès
2018-02-05[native_compute] Remove useless conversion to list in reification.Maxime Dénès
2018-02-05Merge PR #6653: [vernac] Remove VernacGoal, allow anonymous definitions in ↵Maxime Dénès
VernacDefinition
2018-02-05Merge PR #6654: CI: Run coqchk on IrisMaxime Dénès
2018-02-05Merge PR #6652: Allow vernacular controls before focus selectorMaxime 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-01Merge PR #6670: Delete duplicate lineMaxime Dénès
2018-02-01Merge PR #6675: [proofview] enter_one: add __LOC__ argument to get relevant ↵Maxime Dénès
error msg
2018-02-01Merge PR #6672: [stm] Move options to a per-document record.Maxime Dénès
2018-02-01Merge PR #6660: [lib] Respect change of options under with/without_option.Maxime Dénès
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-31CI: Run coqchk on IrisRalf Jung
2018-01-31Proofview: enter_one: add __LOC__ argument to get relevant error msgEnrico 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-31Merge PR #6601: Circle CI: fix cache selection.Maxime Dénès
2018-01-31Merge PR #6641: ci-compcert.sh: use default value for NJOBS when installing ↵Maxime Dénès
menhir.
2018-01-31Merge PR #6663: [toplevel] Refactor load path handling.Maxime Dénès
2018-01-31Merge PR #6656: Fix #5747: "make validate" fails with "bad recursive trees"Maxime Dénès
2018-01-31Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Maxime Dénès
2018-01-30Delete duplicate linePaul 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-30Put default value for NJOBS in ci-common.Gaëtan Gilbert
2018-01-30Adding an overlay for Equations.Pierre-Marie Pédrot
2018-01-30Merge PR #6666: Fix reduction of primitive projections on coinductive ↵Maxime Dénès
records for cbv and native_compute
2018-01-30Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projectionsMaxime Dénès
2018-01-30Merge PR #6636: Stop running duplicate Travis jobs on pull requests.Maxime Dénès
2018-01-30Merge PR #6605: Safer VM interfacesMaxime Dénès
2018-01-30Merge PR #6644: Use travis_retry on apt-get updateMaxime Dénès
2018-01-29Add test case for #5286.Maxime Dénès
2018-01-29[cbv] Fix evaluation of cofixpoints under primitive projections.Maxime Dénès
Fixes #5286 (last remaining part).
2018-01-29[native_compute] Fix evaluation of cofixpoints under primitive projections.Maxime Dénès
2018-01-29[toplevel] Refactor load path handling.Emilio Jesus Gallego Arias
We refactor top-level load path handling. This is in preparation to make load paths become local to a particular document. To this effect, we introduce a new data type `coq_path` that includes the full specification of a load path: ``` type add_ml = AddNoML | AddTopML | AddRecML type vo_path_spec = { unix_path : string; (* Filesystem path contaning vo/ml files *) coq_path : Names.DirPath.t; (* Coq prefix for the path *) implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) } type coq_path_spec = | VoPath of vo_path_spec | MlPath of string type coq_path = { path_spec: coq_path_spec; recursive: bool; } ``` Then, initialization of load paths is split into building a list of load paths and actually making them effective. A future commit will make thus the list of load paths a parameter for document creation. This API is necessarily internal [for now] thus I don't think a changes entry is needed.
2018-01-26allow vernacular controls before focus selector, issue #6587Paul Steckler
2018-01-26Safer VM interfacesMaxime Dénès
We separate functions dealing with VM values (vmvalues.ml) and interfaces of the bytecode interpreter (vm.ml). Only the former relies on untyped constructions. This also makes the VM architecture closer to the one of native_compute, another patch could probably try to share more code between the two for conversion and reification (not trivial, though). This is also preliminary work for integers and arrays.
2018-01-25Add test case for #5747Maxime Dénès
2018-01-25[checker] Avoid relying on canonical names.Maxime Dénès
Fixes #5747: "make validate" fails with "bad recursive trees"
2018-01-25[checker] Remove duplicated functionMaxime Dénès
2018-01-25[checker] Better error message for bad recursive treesMaxime Dénès
2018-01-25Add a comment referencing travis issue numbersJason Gross
2018-01-25Merge PR #6642: fix space in coqchk errorMaxime Dénès
2018-01-25Merge PR #6650: Remove dead code from funind.Maxime Dénès
2018-01-25Merge PR #6626: [readme] Add DOI badge.Maxime Dénès
2018-01-25Merge PR #6620: Fix #6591: anomaly when using selectors outside of a proof.Maxime Dénès
2018-01-24fix space in coqchk errorRalf Jung
2018-01-24Remove dead code from funind.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-09 23:12:39 +0000