aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprGravatar Maxime Dénès2018-01-16
|\
* \ Merge PR #6466: Replace md5sum/md5 calls by an OCaml programGravatar Maxime Dénès2018-01-16
|\ \
* \ \ Merge PR #6551: Bracket with goal selectorGravatar Maxime Dénès2018-01-16
|\ \ \
| | * | Avoid shell backticks and improve md5sum.ml error messagesGravatar Jacques-Pascal Deplaix2018-01-15
| | | |
| * | | More tests on brackets with goal selectors (including failures).Gravatar Théo Zimmermann2018-01-15
| | | |
| * | | Add test-suite file for bracket with goal selector.Gravatar Théo Zimmermann2018-01-15
| | | |
* | | | Merge PR #6578: Remove references to deleted Unicode.Unsupported exceptionGravatar Maxime Dénès2018-01-13
|\ \ \ \
* \ \ \ \ Merge PR #6581: Added newline at the end of usage of coqdep.Gravatar Maxime Dénès2018-01-13
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6564: Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Maxime Dénès2018-01-13
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6483: Strong invariants in polymorphic definitionsGravatar Maxime Dénès2018-01-12
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6288: Interfaces for checker and IDE.Gravatar Maxime Dénès2018-01-12
|\ \ \ \ \ \ \ \
| | * | | | | | | Adding a custom Travis overlay for HoTT.Gravatar Pierre-Marie Pédrot2018-01-11
| | | | | | | | |
| | * | | | | | | Enforce that polymorphic definitions do not generate internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | * | | | | | Document test-suite PRINT_LOGS.Gravatar Gaëtan Gilbert2018-01-11
| | | | | | | | |
| | | * | | | | | Fix undefined variables in test-suite/Makefile + add PRINT_LOGSGravatar Gaëtan Gilbert2018-01-11
| |_|/ / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | PRINT_LOGS can be used for interactive calls, eg make report PRINT_LOGS=1
* | | | | | | | Merge PR #6557: First stab at documenting the test suite.Gravatar Maxime Dénès2018-01-11
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #6552: [PR template] Remove the relative link to CHANGES.Gravatar Maxime Dénès2018-01-11
|\ \ \ \ \ \ \ \ \
| | | | | * | | | | Added newline at the end of usage of coqdep.Gravatar Bernhard Schommer2018-01-11
| |_|_|_|/ / / / / |/| | | | | | | |
| | | | * | | | | Force polymorphic definitions to have no internal constraints.Gravatar Pierre-Marie Pédrot2018-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | * | | | Remove references to removed Unicode.UnsupportedGravatar Jasper Hugunin2018-01-11
| |_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | This exception was removed in [on Oct 13, 2016](https://github.com/coq/coq/commit/57c6ffd23836364168ffd1c66dbddbecf830c7c6#diff-297bc4c11289c2c0ed18d5eebf817c47).
| | * | | | | | Lint and remove redundant lineGravatar Jasper Hugunin2018-01-11
| | | | | | | |
| | | * | | | | Add interfaces for IDE and remove dead code.Gravatar Maxime Dénès2018-01-10
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Should fix #6177, which was triggered by lonely .ml files.
| | | * | | | | Add interfaces for checker and remove dead code.Gravatar Maxime Dénès2018-01-10
| |_|/ / / / / |/| | | | | |
* | | | | | | Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] labelGravatar Maxime Dénès2018-01-10
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6570: [meta] Fix typo on Coq's META file following #6444.Gravatar Maxime Dénès2018-01-10
|\ \ \ \ \ \ \ \ | |_|_|_|/ / / / |/| | | | | | |
| | | | * | | | Add comments by @psteckler to test-suite/README.mdGravatar Jasper Hugunin2018-01-10
| | | | | | | |
| * | | | | | | [meta] Fix typo on Coq's META file following #6444.Gravatar Emilio Jesus Gallego Arias2018-01-09
|/ / / / / / /
| | | | | | * [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
| | | | | | |
* | | | | | | Merge PR #6532: Fix mli-doc issue #6531Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #6489: Update PNGs; mention async error handling; change query ↵Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | window to query pane in text
* \ \ \ \ \ \ \ \ Merge PR #6497: Add optimize_heap tactic for #6488Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6549: Normalize package namesGravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6533: Update the lower-bound of the lablgtk dependency.Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #6425: Cleanup universes in the kernelGravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6530: Ignore generated test-suite/output/MExtraction.outGravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6517: Trim more trailing whitespace in coq-makefile timing testGravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6527: Update backport script for more control.Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6526: Fixing various typos in the Credits chapter.Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | * | | | | | github-check-prs.py: print PR URLs when needed.Gravatar Gaëtan Gilbert2018-01-08
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | * | | | | | github-check-prs.py: Strip spaces from token from command lineGravatar Gaëtan Gilbert2018-01-08
| | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | * | | | | | github-check-prs.py: command line option to get token from a fileGravatar Gaëtan Gilbert2018-01-08
| | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | Merge PR #6510: Document between and exists_between types.Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | | | | Document between and exists_between types.Gravatar Ismail2018-01-08
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | Merge PR #6518: Fix build of micromega & nsatz with OCaml 4.06Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #6501: Document use of ocamldebug from the command line in ↵Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Cygwin/Windows
| | | | | | | | | | | | | | | | | * | | | Mention -B argument of make to rerun testsGravatar Jasper Hugunin2018-01-07
| | | | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | | * | | | First stab at documenting the test suite.Gravatar Jasper Hugunin2018-01-06
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | |
| | | | | | | | | | | | | | | | * | | | [PR template] Remove the relative link.Gravatar Théo Zimmermann2018-01-05
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was actually pointing to https://github.com/CHANGES.
| | | | | | | | | | | | | | | | * | | Documentation and CHANGES for bracket with goal selector.Gravatar Théo Zimmermann2018-01-05
| | | | | | | | | | | | | | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 04:04:13 +0000