aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-19Add test-suite file for issue #6617.Cyprien Mangin
2018-01-19Fix context handling of fix and cofix in Ltac subterm matching.Cyprien Mangin
2018-01-19Define EConstr version of [push_rec_types].Cyprien Mangin
2018-01-18add flash infos about wrap, not found, no. of replacements, no. of finds, ↵Paul Steckler
issue #6452
2018-01-18Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.Maxime Dénès
2018-01-18Merge PR #6448: Cleanup and add debug printers a bitMaxime Dénès
2018-01-17Merge PR #6600: Update configure.ml to only warn on lablgtk >= 2.16.0 and < ↵Maxime Dénès
2.18.3
2018-01-17Merge PR #6593: Add plugins to META.coqMaxime Dénès
2018-01-17Merge PR #6298: Fix #6297: handle constraints like (u+1 <= Set/Prop)Maxime Dénès
2018-01-17Merge PR #6584: Implement the strategy mechanism in the checkerMaxime Dénès
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-16Update lablgtk check to be more generalJason Gross
2018-01-16Rename coq.ltac to coq.plugins.ltac in META.coqCyprien Mangin
2018-01-16Update configure.ml to only warn on lablgtk 2.16.0Jason Gross
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 09:45:35 +0000