aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* | | | | | | | | | Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Gravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #6584: Implement the strategy mechanism in the checkerGravatar Maxime Dénès2018-01-17
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | * | Add CHANGES entryGravatar Jasper Hugunin2018-01-17
| | | | | | | | | | | |
| | | | | | | | | | * | Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionGravatar Jasper Hugunin2018-01-17
| | | | | | | | | | | |
| | | | | | * | | | | | Add CHANGES entryGravatar Jasper Hugunin2018-01-17
| | | | | | | | | | | |
| | | | | | * | | | | | Add a test that `prod_applist_assum` reduces the right number of let-insGravatar Jasper Hugunin2018-01-17
| | | | | | | | | | | |
| | | | | | * | | | | | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
| | | | | | | |_|_|/ / | | | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
| | | | * | | | | | | Update lablgtk check to be more generalGravatar Jason Gross2018-01-16
| | | | | | | | | | |
| | | * | | | | | | | Rename coq.ltac to coq.plugins.ltac in META.coqGravatar Cyprien Mangin2018-01-16
| | | | | | | | | | |
| | | | * | | | | | | Update configure.ml to only warn on lablgtk 2.16.0Gravatar Jason Gross2018-01-16
| | | | | |/ / / / / | | | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The Launchpad packages for lablgtk2 are misconfigured to report 2.16.0 even for much newer versions. This makes building Coq on Ubuntu impossible without modifying configure. This commit fixes that problem. See https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 for the upstream bug. This closes #6585
| | | | | | | | | * merge-pr.sh: use git diff --quietGravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | |
| | | | | | | | | * Source basic overlay before user overlays.Gravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | |
| | | | | | | | | * Cleanup shell expansions and quoting.Gravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | |
| | | | | | | | | * Simplify logic and streamline lint-repository.shGravatar Gaëtan Gilbert2018-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We inline should-check-whitespace.sh in check-eof-newline.sh simplifying the find invocation.
* | | | | | | | | | Merge PR #6590: Fix the wrapper around ocamldebug.Gravatar Maxime Dénès2018-01-16
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ 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
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | |
| | | | | | | * | | | | | Add plugins to META.coqGravatar Cyprien Mangin2018-01-16
| |_|_|_|_|_|/ / / / / / |/| | | | | | | | | | |
| | | | * | | | | | | | Fix the wrapper around ocamldebug.Gravatar Pierre-Marie Pédrot2018-01-15
| |_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Since 5ffa147, there is a new clib folder that needed to be added to the set of includes of ocamldebug
| | * | | | | | | | | 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
| | | | | | | | | | |
| | | | * | | | | | | Actually use the strategy information in the checker.Gravatar Pierre-Marie Pédrot2018-01-14
| | | | | | | | | | |
| | | | * | | | | | | Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
| |_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet.
* | | | | | | | | | 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
|/ / / / / / / / / / / /
| | | | | | | | | | | * Cleanup conditional in lint-repository.shGravatar Gaëtan Gilbert2018-01-08
| | | | | | | | | | | |
| | | | | | | | | | * | Stop talking about debian in "A note about rlwrap"Gravatar Gaëtan Gilbert2018-01-08
| | | | | | | | | | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Debian stable version is 0.42-3 right now.
| | | | | | * | | | | [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
| | | | | | | | | | |
* | | | | | | | | | | Merge PR #6532: Fix mli-doc issue #6531Gravatar Maxime Dénès2018-01-08
|\ \ \ \ \ \ \ \ \ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 19:44:23 +0000