aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-05-13[travis] Move VST to required suite.Emilio Jesus Gallego Arias
2017-05-13Uniformity of style for selecting plural or not; spacing for comma.Hugo Herbelin
2017-05-13Typo in a comment of plugin Quote.Hugo Herbelin
2017-05-13Aligning on standard layout of CHANGES.Hugo Herbelin
2017-05-11Add documentation for Set Ltac Batch DebugJason Gross
2017-05-11Documenting Printing Compact Contexts + CHANGESPierre Courtieu
2017-05-11Obligations shrinking: shrink abstraction tooMatthieu Sozeau
2017-05-11Merge PR#594: An example showing the benefit of EconstrMaxime Dénès
2017-05-11Merge PR#373: A refined solution to the beta-iota discrepancies between 8.4 ↵Maxime Dénès
and 8.5/8.6 "refine"
2017-05-11Merge PR#572: Replacing costly merges in UGraph.Maxime Dénès
2017-05-11Remove an unused open introduced by the previous commit.Maxime Dénès
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-10Switch bedrock to mit-plv baseJason Gross
2017-05-10Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in ↵Maxime Dénès
"Print Assumptions".
2017-05-10Moving code for miscellaneous tests to specific files.Hugo Herbelin
The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.
2017-05-10A more regular naming of variables in test-suite Makefile.Hugo Herbelin
2017-05-10Adding tests for testing exit status and #use"include".Hugo Herbelin
2017-05-10Cleaning old untested not any more interesting testing files.Hugo Herbelin
2017-05-09Merge PR#591: Add bmsherman/topology to the ciMaxime Dénès
2017-05-09Put .travis.yml in alphabetical orderJason Gross
2017-05-09Merge PR#619: Fix warnings in top_printersMaxime Dénès
2017-05-09Merge PR#612: Set Ltac Batch DebugMaxime Dénès
2017-05-09Merge PR#606: Added an option Set Debug CbvMaxime Dénès
2017-05-09Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated.Maxime Dénès
2017-05-09Merge PR#615: coqtop -help: don't die if coqlib can't be foundMaxime Dénès
2017-05-09Merge PR#609: Fix bug #3659: -time should understand multibyte encodings.Maxime Dénès
2017-05-09Merge PR#617: [toplevel] Fix a couple of logical errors in error printing.Maxime Dénès
2017-05-09Prevent user-defined ring morphisms from ever being evaluated.Guillaume Melquiond
2017-05-08Fix warnings in top_printersGaetan Gilbert
Note that [@@@ocaml.warning "-32"] caused an error with Drop. It was put there because I didn't realise the warning was about a real issue.
2017-05-05[toplevel] Fix a couple of logical errors in error printing.Emilio Jesus Gallego Arias
In 4abb41d008fc754f21916dcac9cce49f2d04dd6d we switched back to use exceptions for error printing. However a couple of mistakes were present in that commit: - We wrongly absorbed the exception on `Vernac.compile`. However, it should be propagated as the caller will correctly print the error now. This introduced a critical bug as now `coqc` return the wrong exit status on error, breaking all sort of things. - We printed parsing exceptions twice; now it is not necessary to print the exception in the parsing handler as it will be propagated. I've checked this commit versus all previously reported bugs and it seems to work; we should definitively add a test-suite case to check that the exit code of `coqc` is correct, plus several other cases such as bugs https://coq.inria.fr/bugs/show_bug.cgi?id=5467 https://coq.inria.fr/bugs/show_bug.cgi?id=5485 https://coq.inria.fr/bugs/show_bug.cgi?id=5484 etc... See also PR #583
2017-05-05Remove dead code and unused open.Maxime Dénès
2017-05-05Merge PR#558: Adding a fold_glob_constr_with_binders combinatorMaxime Dénès
2017-05-05Remove two unused opens.Maxime Dénès
2017-05-05Merge PR#598: Removing dead code in Autorewrite.Maxime Dénès
2017-05-05Fix bug #3659: -time should understand multibyte encodings.Pierre-Marie Pédrot
We assume Coq always outputs UTF-8 (is it really the case?) and cut strings after 30 UTF-8 characters instead of using the standard String function.
2017-05-05Documenting Option.List.find.Hugo Herbelin
2017-05-05Cosmetic: unifying style within option.ml.Hugo Herbelin
2017-05-05Upgrading some local function as a general-purpose combinator Option.List.map.Hugo Herbelin
2017-05-05Adding a test-suite pattern-unification example that Econstr fixed.Hugo Herbelin
2017-05-05Merge PR#610: Improve documentation of assert / pose proof / specialize.Maxime Dénès
2017-05-05Merge PR#605: Report a useful error for dependent inductionMaxime Dénès
2017-05-05coqtop -help: don't die if coqlib can't be foundGaetan Gilbert
2017-05-05Merge PR#454: Printing unfocussed goals and toward a pg plugin.Maxime Dénès
2017-05-05Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteMaxime Dénès
2017-05-05Remove unused open.Maxime Dénès
2017-05-05Merge PR#544: Anonymous universesMaxime Dénès
2017-05-05Adapted to EConstr.Pierre Courtieu
2017-05-04Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵Hugo Herbelin
batch mode.
2017-05-04Improve documentation of assert / pose proof / specialize.Théo Zimmermann
This commits documents the as clause of specialize and that the as clause of pose proof is optional. It also mentions a feature of assert ( := ) that was available since 8.5 and was mentionned by @herbelin in: https://github.com/coq/coq/pull/248#issuecomment-297970503
2017-05-04Warning removed.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-04 00:53:57 +0000