aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
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-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-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
2018-01-24Fix #6621: Anomaly on fixpoint with primitive projectionsMaxime Dénès
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.
2018-01-23Delay installing packagesJason Gross
sudo apt-get install will fail on gcc-multilib if apt-get update cannot fetch launchpad, so instead we delay installing these packages.
2018-01-23Use travis_retry on apt-get updateJason Gross
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.
2018-01-23Stop running duplicate Travis jobs on pull requests.Théo Zimmermann
These tests are already done by CircleCI.
2018-01-23Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants ↵Maxime Dénès
for primitive projections
2018-01-23Merge PR #6628: [printing] Remove duplicate definitions of pr_lident and ↵Maxime Dénès
pr_lname
2018-01-23Merge PR #6629: Archive COMPATIBILITYMaxime Dénès
2018-01-23Merge PR #6568: Cleanup scriptsMaxime Dénès
2018-01-22Fix #6591: anomaly when using selectors outside of a proof.Cyprien Mangin
When asking for a hint about bullets, we check that there is an ongoing proof.
2018-01-22[readme] Add DOI badge.Emilio Jesus Gallego Arias
2018-01-22Archive COMPATIBILITY.Théo Zimmermann
2018-01-22Move the mention of the removal of Qed exporting at the right place.Théo Zimmermann
2018-01-22Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Maxime Dénès
2018-01-22Merge PR #6625: Update location on tab switch, issue 6624Maxime Dénès
2018-01-22Merge PR #6576: generate both binary and text annotationsMaxime Dénès
2018-01-22Merge PR #6550: Remove outdated note about rlwrap in setup.txtMaxime Dénès
2018-01-22Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.Maxime Dénès
2018-01-22Merge PR #6575: Add flash infos for find and replaceMaxime Dénès
2018-01-22Merge PR #6506: Fast rel lookupMaxime Dénès
2018-01-22[printing] Remove duplicate definitions of pr_lident and pr_lnameVincent Laporte
2018-01-20Adding a test for coqchk bug #6619.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-19 18:14:29 +0000