aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-16Source basic overlay before user overlays.Gaëtan Gilbert
2018-01-16Cleanup shell expansions and quoting.Gaëtan Gilbert
2018-01-16Simplify logic and streamline lint-repository.shGaëtan Gilbert
We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
2018-01-16Merge PR #6590: Fix the wrapper around ocamldebug.Maxime Dénès
2018-01-16Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprMaxime Dénès
2018-01-16Merge PR #6466: Replace md5sum/md5 calls by an OCaml programMaxime Dénès
2018-01-16Merge PR #6551: Bracket with goal selectorMaxime Dénès
2018-01-16Add plugins to META.coqCyprien Mangin
2018-01-15Fix the wrapper around ocamldebug.Pierre-Marie Pédrot
Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug
2018-01-15Avoid shell backticks and improve md5sum.ml error messagesJacques-Pascal Deplaix
2018-01-15More tests on brackets with goal selectors (including failures).Théo Zimmermann
2018-01-15Add test-suite file for bracket with goal selector.Théo Zimmermann
2018-01-14Actually use the strategy information in the checker.Pierre-Marie Pédrot
2018-01-14Store the conversion oracle in constant and inductive definitions.Pierre-Marie Pédrot
We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet.
2018-01-13Merge PR #6578: Remove references to deleted Unicode.Unsupported exceptionMaxime Dénès
2018-01-13Merge PR #6581: Added newline at the end of usage of coqdep.Maxime Dénès
2018-01-13Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSMaxime Dénès
2018-01-12Merge PR #6483: Strong invariants in polymorphic definitionsMaxime Dénès
2018-01-12Merge PR #6288: Interfaces for checker and IDE.Maxime Dénès
2018-01-11Adding a custom Travis overlay for HoTT.Pierre-Marie Pédrot
2018-01-11Enforce that polymorphic definitions do not generate internal constraints.Pierre-Marie Pédrot
In practice, we only send to the kernel polymorphic definitions whose side-effects have been exported first, and furthermore their bodies have already been forced. Therefore, no constraints are generated by the kernel. Nonetheless, it might be desirable in the future to also defer computation of polymorphic proofs whose constraints have been explicited in the type. It is not clear when this is going to be implemented. Nonetheless, the current check is not too drastic as it only prevents monomorphic side-effects to appear inside polymorphic opaque definitions. The only way I know of to trigger such a situation is to generate a scheme in a proof, as even abstract is actually preserving the polymorphism status of the surrounding proof. It would be possible to work around such rare instances anyways. As for internal constraints generated by a potentially deferred polymorphic body, it is easy to check that they are a subset of the exported ones at a higher level inside the future computation and fail there. So in practice this patch is not too restrictive and it highlights a rather strong invariant of the kernel code.
2018-01-11Document test-suite PRINT_LOGS.Gaëtan Gilbert
2018-01-11Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGaëtan Gilbert
PRINT_LOGS can be used for interactive calls, eg make report PRINT_LOGS=1
2018-01-11Merge PR #6557: First stab at documenting the test suite.Maxime Dénès
2018-01-11Merge PR #6552: [PR template] Remove the relative link to CHANGES.Maxime Dénès
2018-01-11Added newline at the end of usage of coqdep.Bernhard Schommer
2018-01-11Force polymorphic definitions to have no internal constraints.Pierre-Marie Pédrot
The main contender was the abstract tactic that was generating useless constraints for polymorphic subproofs that happened to contain themselves monomorphic subproofs. We had to fix the test-suite for one particular corner-case instance that looked more like a bug than anything else.
2018-01-11Remove references to removed Unicode.UnsupportedJasper Hugunin
This exception was removed in [on Oct 13, 2016](https://github.com/coq/coq/commit/57c6ffd23836364168ffd1c66dbddbecf830c7c6#diff-297bc4c11289c2c0ed18d5eebf817c47).
2018-01-11Lint and remove redundant lineJasper Hugunin
2018-01-10Add interfaces for IDE and remove dead code.Maxime Dénès
Should fix #6177, which was triggered by lonely .ml files.
2018-01-10Add interfaces for checker and remove dead code.Maxime Dénès
2018-01-10Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] labelMaxime Dénès
2018-01-10Merge PR #6570: [meta] Fix typo on Coq's META file following #6444.Maxime Dénès
2018-01-10Fix ci-all targetGaëtan Gilbert
2018-01-10Add comments by @psteckler to test-suite/README.mdJasper Hugunin
2018-01-09[meta] Fix typo on Coq's META file following #6444.Emilio Jesus Gallego Arias
2018-01-09[Backport script] Check .mli files are not changed.Théo Zimmermann
2018-01-08Cleanup conditional in lint-repository.shGaëtan Gilbert
2018-01-08Stop talking about debian in "A note about rlwrap"Gaëtan Gilbert
Debian stable version is 0.42-3 right now.
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2018-01-08Merge PR #6532: Fix mli-doc issue #6531Maxime Dénès
2018-01-08Merge PR #6489: Update PNGs; mention async error handling; change query ↵Maxime Dénès
window to query pane in text
2018-01-08Merge PR #6497: Add optimize_heap tactic for #6488Maxime Dénès
2018-01-08Merge PR #6549: Normalize package namesMaxime Dénès
2018-01-08Merge PR #6533: Update the lower-bound of the lablgtk dependency.Maxime Dénès
2018-01-08Merge PR #6425: Cleanup universes in the kernelMaxime Dénès
2018-01-08Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scriptsMaxime Dénès
2018-01-08Merge PR #6530: Ignore generated test-suite/output/MExtraction.outMaxime Dénès
2018-01-08Merge PR #6517: Trim more trailing whitespace in coq-makefile timing testMaxime Dénès
2018-01-08Merge PR #6527: Update backport script for more control.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-20 02:24:07 +0000