aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| | | | | * | | | | | | | | Add test case for #5286.Gravatar Maxime Dénès2018-01-29
| | | | | | | | | | | | | |
| | | | | * | | | | | | | | [cbv] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #5286 (last remaining part).
| | | | | * | | | | | | | | [native_compute] Fix evaluation of cofixpoints under primitive projections.Gravatar Maxime Dénès2018-01-29
| |_|_|_|/ / / / / / / / / |/| | | | | | | | | | | |
| | | | | | | * | | | | | [toplevel] Refactor load path handling.Gravatar Emilio Jesus Gallego Arias2018-01-29
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | | * | allow vernacular controls before focus selector, issue #6587Gravatar Paul Steckler2018-01-26
| |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | |
| | * | | | | | | | | Safer VM interfacesGravatar Maxime Dénès2018-01-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | | | | | * document the Fail commandGravatar Paul Steckler2018-01-25
| |_|_|_|_|_|_|_|_|/ |/| | | | | | | | |
| | | | | | * | | | Add test case for #5747Gravatar Maxime Dénès2018-01-25
| | | | | | | | | |
| | | | | | * | | | [checker] Avoid relying on canonical names.Gravatar Maxime Dénès2018-01-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Fixes #5747: "make validate" fails with "bad recursive trees"
| | | | | | * | | | [checker] Remove duplicated functionGravatar Maxime Dénès2018-01-25
| | | | | | | | | |
| | | | | | * | | | [checker] Better error message for bad recursive treesGravatar Maxime Dénès2018-01-25
| |_|_|_|_|/ / / / |/| | | | | | | |
| * | | | | | | | Add a comment referencing travis issue numbersGravatar Jason Gross2018-01-25
| | | | | | | | |
* | | | | | | | | Merge PR #6642: fix space in coqchk errorGravatar Maxime Dénès2018-01-25
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6650: Remove dead code from funind.Gravatar Maxime Dénès2018-01-25
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6626: [readme] Add DOI badge.Gravatar Maxime Dénès2018-01-25
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #6620: Fix #6591: anomaly when using selectors outside of a proof.Gravatar Maxime Dénès2018-01-25
|\ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | |
| | | | * | | | | | | fix space in coqchk errorGravatar Ralf Jung2018-01-24
| |_|_|/ / / / / / / |/| | | | | | | | |
| | | * | | | | | | Remove dead code from funind.Gravatar Maxime Dénès2018-01-24
| |_|/ / / / / / / |/| | | | | | | |
| | | | | * | | | Fix #6621: Anomaly on fixpoint with primitive projectionsGravatar Maxime Dénès2018-01-24
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The implementation of the subterm relation for primitive projections was a bit wrong. I found the problem independently of this bug, and tried to see if a proof of False could be derived, but I don't think so, due to another check (check_is_subterm) that saves the kernel at the last minute.
| | | * | | | | Delay installing packagesGravatar Jason Gross2018-01-23
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | sudo apt-get install will fail on gcc-multilib if apt-get update cannot fetch launchpad, so instead we delay installing these packages.
| | | * | | | | Use travis_retry on apt-get updateGravatar Jason Gross2018-01-23
| |_|/ / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Script modified from https://unix.stackexchange.com/questions/175146/apt-get-update-exit-status I stuck the code in "install" rather than "before_install" so that the lint target didn't need to be changed. I also haven't touched the targets that add more packages; I'll leave that to someone who knows more about the "&" and "*" syntax being used in the configuration.
| | | * | | | Stop running duplicate Travis jobs on pull requests.Gravatar Théo Zimmermann2018-01-23
| |_|/ / / / |/| | | | | | | | | | | | | | | | | These tests are already done by CircleCI.
* | | | | | Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵Gravatar Maxime Dénès2018-01-23
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | for primitive projections
* \ \ \ \ \ \ Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and ↵Gravatar Maxime Dénès2018-01-23
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | pr_lname
* \ \ \ \ \ \ \ Merge PR #6629: Archive COMPATIBILITYGravatar Maxime Dénès2018-01-23
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6568: Cleanup scriptsGravatar Maxime Dénès2018-01-23
|\ \ \ \ \ \ \ \ \
| | | | | * | | | | Fix #6591: anomaly when using selectors outside of a proof.Gravatar Cyprien Mangin2018-01-22
| | | | | | |_|_|/ | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When asking for a hint about bullets, we check that there is an ongoing proof.
| | | | | | * | | [readme] Add DOI badge.Gravatar Emilio Jesus Gallego Arias2018-01-22
| | | | | |/ / /
| | * | | | | | Archive COMPATIBILITY.Gravatar Théo Zimmermann2018-01-22
| | | | | | | |
| | * | | | | | Move the mention of the removal of Qed exporting at the right place.Gravatar Théo Zimmermann2018-01-22
| | | |_|/ / / | | |/| | | |
* | | | | | | Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6625: Update location on tab switch, issue 6624Gravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6576: generate both binary and text annotationsGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6550: Remove outdated note about rlwrap in setup.txtGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Gravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6575: Add flash infos for find and replaceGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6506: Fast rel lookupGravatar Maxime Dénès2018-01-22
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | |
| | | | | | | | | * | | | [printing] Remove duplicate definitions of pr_lident and pr_lnameGravatar Vincent Laporte2018-01-22
| |_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | |
| | | | | | | | | * | | Adding a test for coqchk bug #6619.Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | | | | | | |
| | | | | | | | | * | | Fix #6618: coqchk fails with "ill-typed term".Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Primitive projections were not correctly unfolded, leading to failure of conversion checks in some cases. The kernel was strangely not affected by this bug, and it was probably a remnant of some vestigial code.
| | | | | | | | | * | | Remove dead code in Environ.Gravatar Pierre-Marie Pédrot2018-01-20
| |_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The constant_value function was actually not behaving the same as constant_value_in w.r.t. projections. The former was not used, and the only place that used the latter was in Tacred and was statically insensitive to the use of projections.
| | | | | * | | | | | -annotate deprecated. New options: -annot, -bin-annotGravatar Vadim Zaliva2018-01-19
| | | | | | | | | | |
| | | | | | * | | | | update location on tab switch, issue 6624Gravatar Paul Steckler2018-01-19
| |_|_|_|_|/ / / / / |/| | | | | | | | |
| | | * | | | | | | Add test-suite file for issue #6617.Gravatar Cyprien Mangin2018-01-19
| | | | | | | | | |
| | | * | | | | | | Fix context handling of fix and cofix in Ltac subterm matching.Gravatar Cyprien Mangin2018-01-19
| | | | | | | | | |
| | | * | | | | | | Define EConstr version of [push_rec_types].Gravatar Cyprien Mangin2018-01-19
| | | | | | | | | |
| | * | | | | | | | add flash infos about wrap, not found, no. of replacements, no. of finds, ↵Gravatar Paul Steckler2018-01-18
| |/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | issue #6452
* | | | | | | | | Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Maxime Dénès2018-01-18
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6448: Cleanup and add debug printers a bitGravatar Maxime Dénès2018-01-18
|\ \ \ \ \ \ \ \ \ \ | |_|_|/ / / / / / / |/| | | | | | | | |
* | | | | | | | | | Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < ↵Gravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 2.18.3
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 06:10:23 +0000