| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-17 | Travis: add -warn-error targets (standard and 4.04.1 ocaml) | Gaetan Gilbert | |
| 2017-05-17 | Travis: deduplicate package list for coqide+documentation targets | Gaetan Gilbert | |
| 2017-05-17 | Travis: do not run the tests if building Coq fails | Gaetan Gilbert | |
| 2017-05-17 | Merge PR#636: Miscellaneous typos, dead code, etc. | Maxime Dénès | |
| 2017-05-17 | Merge PR#639: Stop using auto with * in two proofs. | Maxime Dénès | |
| 2017-05-16 | Stop using auto with * in two proofs. | Théo Zimmermann | |
| auto with * is an overkill for people who do not care to understand what they really need. In these two cases, one lemma which was available in the typeclass_instances hint db. | |||
| 2017-05-16 | Merge PR#626: Add documentation for Set Ltac Batch Debug | Maxime Dénès | |
| 2017-05-16 | Merge PR#629: A couple of simple updates for Travis | Maxime Dénès | |
| 2017-05-15 | Dead code in coqdep. | Hugo Herbelin | |
| Was introduced in 5268efdef, reverted then readded in 1be9c4d. | |||
| 2017-05-15 | Typo in comments of constrintern. | Hugo Herbelin | |
| 2017-05-13 | [travis] Update OCaml to 4.04.1 | Emilio Jesus Gallego Arias | |
| 2017-05-13 | [travis] Move VST to required suite. | Emilio Jesus Gallego Arias | |
| 2017-05-13 | Uniformity of style for selecting plural or not; spacing for comma. | Hugo Herbelin | |
| 2017-05-13 | Typo in a comment of plugin Quote. | Hugo Herbelin | |
| 2017-05-13 | Aligning on standard layout of CHANGES. | Hugo Herbelin | |
| 2017-05-11 | Add documentation for Set Ltac Batch Debug | Jason Gross | |
| 2017-05-11 | Merge PR#594: An example showing the benefit of Econstr | Maxime Dénès | |
| 2017-05-11 | Merge 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-11 | Merge PR#572: Replacing costly merges in UGraph. | Maxime Dénès | |
| 2017-05-11 | Remove an unused open introduced by the previous commit. | Maxime Dénès | |
| 2017-05-11 | Merge PR#201: Transparent abstract | Maxime Dénès | |
| 2017-05-09 | Merge PR#619: Fix warnings in top_printers | Maxime Dénès | |
| 2017-05-09 | Merge PR#612: Set Ltac Batch Debug | Maxime Dénès | |
| 2017-05-09 | Merge PR#606: Added an option Set Debug Cbv | Maxime Dénès | |
| 2017-05-09 | Merge PR#621: Prevent user-defined ring morphisms from ever being evaluated. | Maxime Dénès | |
| 2017-05-09 | Merge PR#615: coqtop -help: don't die if coqlib can't be found | Maxime Dénès | |
| 2017-05-09 | Merge PR#617: [toplevel] Fix a couple of logical errors in error printing. | Maxime Dénès | |
| 2017-05-09 | Prevent user-defined ring morphisms from ever being evaluated. | Guillaume Melquiond | |
| 2017-05-08 | Fix warnings in top_printers | Gaetan 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-05 | Remove dead code and unused open. | Maxime Dénès | |
| 2017-05-05 | Merge PR#558: Adding a fold_glob_constr_with_binders combinator | Maxime Dénès | |
| 2017-05-05 | Remove two unused opens. | Maxime Dénès | |
| 2017-05-05 | Merge PR#598: Removing dead code in Autorewrite. | Maxime Dénès | |
| 2017-05-05 | Documenting Option.List.find. | Hugo Herbelin | |
| 2017-05-05 | Cosmetic: unifying style within option.ml. | Hugo Herbelin | |
| 2017-05-05 | Upgrading some local function as a general-purpose combinator Option.List.map. | Hugo Herbelin | |
| 2017-05-05 | Adding a test-suite pattern-unification example that Econstr fixed. | Hugo Herbelin | |
| 2017-05-05 | Merge PR#610: Improve documentation of assert / pose proof / specialize. | Maxime Dénès | |
| 2017-05-05 | Merge PR#605: Report a useful error for dependent induction | Maxime Dénès | |
| 2017-05-05 | coqtop -help: don't die if coqlib can't be found | Gaetan Gilbert | |
| 2017-05-05 | Merge PR#454: Printing unfocussed goals and toward a pg plugin. | Maxime Dénès | |
| 2017-05-05 | Merge PR#593: Functional choice <-> [inhabited] and [forall] commute | Maxime Dénès | |
| 2017-05-05 | Remove unused open. | Maxime Dénès | |
| 2017-05-05 | Merge PR#544: Anonymous universes | Maxime Dénès | |
| 2017-05-04 | Adding an option "Set Ltac Batch Debug" to additionally run Ltac debug in ↵ | Hugo Herbelin | |
| batch mode. | |||
| 2017-05-04 | Improve 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-04 | Warning removed. | Pierre Courtieu | |
| 2017-05-04 | labelizing arguments | Pierre Courtieu | |
| 2017-05-04 | Adding an option "Printing Unfocused". | Pierre Courtieu | |
| Off by default. + small refactoring of emacs hacks in printer.ml. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |