aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-01-17Add CHANGES entryJasper Hugunin
2018-01-17Add a test that `prod_applist_assum` reduces the right number of let-insJasper Hugunin
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
Fixes #6490. `prod_applist_assum` is copied from `kernel/term.ml` to `engine/termops.ml`, and adjusted to work with econstr. This change uncovered a bug in `Hipattern.match_with_nodep_ind`, where `has_nodep_prod_after` counts both products and let-ins, but was only being passed `mib.mind_nparams`, which does not count let-ins. Replaced with (Context.Rel.length mib.mind_params_ctxt).
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-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-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
2018-01-08Merge PR #6526: Fixing various typos in the Credits chapter.Maxime Dénès
2018-01-08github-check-prs.py: print PR URLs when needed.Gaëtan Gilbert
2018-01-08github-check-prs.py: Strip spaces from token from command lineGaëtan Gilbert
2018-01-08github-check-prs.py: command line option to get token from a fileGaëtan Gilbert
2018-01-08Merge PR #6510: Document between and exists_between types.Maxime Dénès
2018-01-08Document between and exists_between types.Ismail
2018-01-08Merge PR #6518: Fix build of micromega & nsatz with OCaml 4.06Maxime Dénès
2018-01-08Merge PR #6501: Document use of ocamldebug from the command line in ↵Maxime Dénès
Cygwin/Windows
2018-01-07Mention -B argument of make to rerun testsJasper Hugunin
2018-01-06First stab at documenting the test suite.Jasper Hugunin
2018-01-05[PR template] Remove the relative link.Théo Zimmermann
Was actually pointing to https://github.com/CHANGES.
2018-01-04Normalize MacOS installer name.Théo Zimmermann
2018-01-04Normalize Windows installer names.Théo Zimmermann
2018-01-04Update the lower-bound of the lablgtk dependency.Théo Zimmermann
Closes #6509.
2018-01-03add optimize_heap tactic for #6488Paul Steckler
2018-01-03update PNGs; mention async error handling; change query window to query ↵Paul Steckler
pane; use color descriptions
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 16:37:34 +0000