| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-09-30 | Merge branch 'v8.5' into v8.6 | Maxime Dénès | |
| 2016-09-30 | Fix test-suite. | Maxime Dénès | |
| Restore subst output test file modified by mistake. | |||
| 2016-09-30 | Merge remote-tracking branch 'github/pr/302' into v8.6 | Maxime Dénès | |
| Was PR#302: Set the default LtacProf cutoff to 2% | |||
| 2016-09-30 | Merge remote-tracking branch 'github/pr/281' into v8.6 | Maxime Dénès | |
| Was PR#281: Fix indentation of -profile-ltac in -help | |||
| 2016-09-30 | Merge remote-tracking branch 'github/pr/280' into v8.6 | Maxime Dénès | |
| Was PR#280: Document that [Reset Ltac Profile] is not synchronized with the document state | |||
| 2016-09-30 | Restore code ignoring <W> lines in output (camlp5 warnings) | Enrico Tassi | |
| 2016-09-30 | Ignore file names in warning emitted by test-suite/output/* (#5111) | Enrico Tassi | |
| 2016-09-30 | In <= 8.5 compat accept "Arguments f /" even if f has arguments (#5112) | Enrico Tassi | |
| 2016-09-30 | Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimpl | Enrico Tassi | |
| 2016-09-30 | Merge remote-tracking branch 'github/pr/294' into v8.5 | Maxime Dénès | |
| Was PR#294: Make error message more helpful. | |||
| 2016-09-30 | Merge remote-tracking branch 'github/pr/257' into v8.6 | Maxime Dénès | |
| Was PR#257: [checker] Fix/fine tune printing. | |||
| 2016-09-30 | Merge branch 'v8.5' into v8.6 | Maxime Dénès | |
| 2016-09-30 | Merge branch '4762' into v8.5 | Maxime Dénès | |
| Was PR#293: Fix #4762 (eauto weaker than auto). | |||
| 2016-09-30 | Fix #4762. | Cyprien Mangin | |
| 2016-09-29 | Set the default LtacProf cutoff to 2% | Jason Gross | |
| This was the original value from Tobias' code. When a user passes -profile-ltac on the command line, or inserts [Show Ltac Profile] in the document, the most useful default behavior is to not overload them with useless information. When GUI clients want to display fancier profiling information, there is no cost to the user to requiring them to specify what cutoff they want. If the GUI client does not have any special LtacProf handling, the most useful presentation is again the one that cuts off the display at 2% total time. | |||
| 2016-09-29 | Fix bug #4798: compat notations should not modify the parser. | Pierre-Marie Pédrot | |
| This is a quick fix. The Metasyntax module should be thoroughly revised in trunk, because it starts featuring a lot of spaghetti code and redundant data. | |||
| 2016-09-29 | STM: compute the correct state for edited Qed (#5086) | Enrico Tassi | |
| When a proof is 're-opened', the Qed node does not change. Still the STM has to install the old state (where only the future proof has to be updated). This bit was missing. Why was it working: the bug happens only if you reopen the very last proof, i.e. there is no sentence that stays valid after the Qed. If there is such a sentence, its state was computed correctly before, and is not changed. If it is the very last, then the next state is based on the wrong one... | |||
| 2016-09-29 | Arguments: cleanup + detect discrepancy rename/implicit (#3753) | Enrico Tassi | |
| It seems warnings are not taken into account in output/ tests. | |||
| 2016-09-29 | Merge branch 'bug5036' into v8.6 | Matthieu Sozeau | |
| 2016-09-29 | Fix bug #5036 autorewrite, sections and universes | Matthieu Sozeau | |
| Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately). | |||
| 2016-09-29 | Merge branch 'bug4723' into v8.6 | Matthieu Sozeau | |
| 2016-09-29 | Being more informative about the change of behavior of "subst". | Hugo Herbelin | |
| 2016-09-29 | fix bug 3683 : adds references to the web site for the bug tracker | Yves Bertot | |
| in error messages | |||
| 2016-09-29 | Fix bug #5011: Anomaly on [Existing Class]. | Pierre-Marie Pédrot | |
| 2016-09-29 | Fix a bug in subst releaved by an OCaml warning. | Maxime Dénès | |
| 2016-09-29 | test-suite: fix sed on OS X, does not handle + | Matthieu Sozeau | |
| 2016-09-29 | Cleanup API, making inference_hook optional | Matthieu Sozeau | |
| 2016-09-29 | Ncring_initial: avoid a notation overriding | Pierre Letouzey | |
| 2016-09-29 | Extraction: ignore some useless stuff about universes | Pierre Letouzey | |
| 2016-09-29 | Argument : assert does fail if no arg is given (fix #4864) | Enrico Tassi | |
| 2016-09-29 | -profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100) | Enrico Tassi | |
| With this command line flag one can profile ltac in files /and/ trim the results without actually touching the files. | |||
| 2016-09-28 | Ring_theory: avoid overriding a few notations | Pierre Letouzey | |
| 2016-09-28 | ZDivEucl: notations in different scope to avoid a warning | Pierre Letouzey | |
| 2016-09-28 | Adding interface files to Nsatz ML files. | Pierre-Marie Pédrot | |
| 2016-09-28 | Fix bug #4723 and FIXME in API for solve_by_tac | Matthieu Sozeau | |
| This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic. | |||
| 2016-09-28 | Do not stop propagation of signals when Coq is busy (bug #3941). | Guillaume Melquiond | |
| When inserting a character in an already processed buffer, a message is sent to Coq so that the proof is backtracked and the character is inserted. If a second character is inserted while Coq is still busy with the first message, the action is canceled, but the signal is no longer dropped so that the second character is properly inserted. | |||
| 2016-09-28 | Make error message more helpful. | Théo Zimmermann | |
| CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options. | |||
| 2016-09-28 | Warning about similar notations now up to alpha-conversion. | Hugo Herbelin | |
| This allows to define on purpose the very same notation in different files, as currently the notations for *, +, - in Nat.v and Peano.v (with the first one using variables n and m and the second one using the default variables used by Infix, namely x and y). This makes also the "notation-overridden" warning less enigmatic facing two notations which are the same up to the choice of names. | |||
| 2016-09-28 | Typeclass backtracking example by J. Leivant | Matthieu Sozeau | |
| 2016-09-28 | Remove incorrect assertion in cbn (bug #4822). | Guillaume Melquiond | |
| This assertion checked that two arguments in the same position were equal, but in fact, since one might have already been reduced, they are only convertible (which is too costly to check in an assertion). | |||
| 2016-09-28 | Merge remote-tracking branch 'github/pr/232' into v8.6 | Maxime Dénès | |
| Was PR#232: Fix the parsing of goal selectors. | |||
| 2016-09-27 | Fix bug #4553: CoqIDE gives warnings about deprecated GTK features. | Pierre-Marie Pédrot | |
| 2016-09-27 | Fix #5061: Warnings flag has no discernible value | Maxime Dénès | |
| The default value of the warnings flag was printed as an empty string, now replaced by "default". | |||
| 2016-09-27 | Add fixed test-suite file for bug #4527 | Matthieu Sozeau | |
| 2016-09-27 | Fixing #4887 (confusion between using and with in documentation of firstorder). | Hugo Herbelin | |
| 2016-09-27 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2016-09-27 | LtacProf: "Show Ltac Profile CutOff $N" (fix #5080) | Enrico Tassi | |
| It seems we have no grammar rule that parses floats, so I'm parsing an integer, but the whole machinery supports floats. | |||
| 2016-09-26 | Remove spaces from around list notations | Jason Gross | |
| 2016-09-26 | Remove spaces from around vector notations | Jason Gross | |
| 2016-09-26 | Unbreak Ltac [ | .. | ] notation in -compat 8.5 | Jason Gross | |
| Importing VectorNotations breaks `; []`. So we make sure it's not imported by defualt. Some files might be required to `Import VectorDef.VectorNotations` rather than just `Import VectorNotations`. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |