aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
| * | | | Fix test-suite.Gravatar Maxime Dénès2016-09-30
| | | | | | | | | | | | | | | | | | | | Restore subst output test file modified by mistake.
* | | | | Merge remote-tracking branch 'github/pr/302' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ \ | | | | | | | | | | | | | | | | | | Was PR#302: Set the default LtacProf cutoff to 2%
* \ \ \ \ \ Merge remote-tracking branch 'github/pr/281' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#281: Fix indentation of -profile-ltac in -help
* \ \ \ \ \ \ Merge remote-tracking branch 'github/pr/280' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#280: Document that [Reset Ltac Profile] is not synchronized with the document state
* | | | | | | | Restore code ignoring <W> lines in output (camlp5 warnings)Gravatar Enrico Tassi2016-09-30
| | | | | | | |
* | | | | | | | Ignore file names in warning emitted by test-suite/output/* (#5111)Gravatar Enrico Tassi2016-09-30
| | | | | | | |
* | | | | | | | In <= 8.5 compat accept "Arguments f /" even if f has arguments (#5112)Gravatar Enrico Tassi2016-09-30
| | | | | | | |
* | | | | | | | Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimplGravatar Enrico Tassi2016-09-30
| | | | | | | |
| | | | * | | | Merge remote-tracking branch 'github/pr/294' into v8.5Gravatar Maxime Dénès2016-09-30
| | | | |\ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#294: Make error message more helpful.
* | | | | \ \ \ \ Merge remote-tracking branch 'github/pr/257' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#257: [checker] Fix/fine tune printing.
* \ \ \ \ \ \ \ \ \ Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
|\ \ \ \ \ \ \ \ \ \ | | |_|_|_|/ / / / / | |/| | | | | | | |
| * | | | | | | | | Merge branch '4762' into v8.5Gravatar Maxime Dénès2016-09-30
| |\ \ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Was PR#293: Fix #4762 (eauto weaker than auto).
| | * | | | | | | | | Fix #4762.Gravatar Cyprien Mangin2016-09-30
| | | | | | | | | | |
| | | | | | | | | * | LtacProf cutoff is for total percent, not timeGravatar Jason Gross2016-09-29
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
| | | | | | * | | | Set the default LtacProf cutoff to 2%Gravatar Jason Gross2016-09-29
| |_|_|_|_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | Fix bug #4798: compat notations should not modify the parser.Gravatar Pierre-Marie Pédrot2016-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | STM: compute the correct state for edited Qed (#5086)Gravatar Enrico Tassi2016-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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...
* | | | | | | | | Arguments: cleanup + detect discrepancy rename/implicit (#3753)Gravatar Enrico Tassi2016-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It seems warnings are not taken into account in output/ tests.
* | | | | | | | | Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-09-29
|\ \ \ \ \ \ \ \ \
| * | | | | | | | | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
* | | | | | | | | | Merge branch 'bug4723' into v8.6Gravatar Matthieu Sozeau2016-09-29
|\ \ \ \ \ \ \ \ \ \
* | | | | | | | | | | Being more informative about the change of behavior of "subst".Gravatar Hugo Herbelin2016-09-29
| | | | | | | | | | |
| | | | | | | | | * | Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
| | | | | | | | | | |
* | | | | | | | | | | fix bug 3683 : adds references to the web site for the bug trackerGravatar Yves Bertot2016-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | in error messages
* | | | | | | | | | | Fix bug #5011: Anomaly on [Existing Class].Gravatar Pierre-Marie Pédrot2016-09-29
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
| | | * | | | | | | Fix a bug in subst releaved by an OCaml warning.Gravatar Maxime Dénès2016-09-29
| | | |/ / / / / /
* | | | | | | | | test-suite: fix sed on OS X, does not handle +Gravatar Matthieu Sozeau2016-09-29
| | | | | | | | |
| * | | | | | | | Cleanup API, making inference_hook optionalGravatar Matthieu Sozeau2016-09-29
| | | | | | | | |
* | | | | | | | | Ncring_initial: avoid a notation overridingGravatar Pierre Letouzey2016-09-29
| | | | | | | | |
* | | | | | | | | Extraction: ignore some useless stuff about universesGravatar Pierre Letouzey2016-09-29
| | | | | | | | |
* | | | | | | | | Argument : assert does fail if no arg is given (fix #4864)Gravatar Enrico Tassi2016-09-29
| | | | | | | | |
* | | | | | | | | -profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)Gravatar Enrico Tassi2016-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | With this command line flag one can profile ltac in files /and/ trim the results without actually touching the files.
* | | | | | | | | Ring_theory: avoid overriding a few notationsGravatar Pierre Letouzey2016-09-28
| | | | | | | | |
* | | | | | | | | ZDivEucl: notations in different scope to avoid a warningGravatar Pierre Letouzey2016-09-28
| | | | | | | | |
* | | | | | | | | Adding interface files to Nsatz ML files.Gravatar Pierre-Marie Pédrot2016-09-28
| | | | | | | | |
| * | | | | | | | Fix bug #4723 and FIXME in API for solve_by_tacGravatar Matthieu Sozeau2016-09-28
| |/ / / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This avoids leakage of universes. Also makes Program Lemma/Fact work again, it tries to solve the remaining evars using the obligation tactic.
* | | | | | | | Do not stop propagation of signals when Coq is busy (bug #3941).Gravatar Guillaume Melquiond2016-09-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | | | | | * | Make error message more helpful.Gravatar Théo Zimmermann2016-09-28
| | | |_|_|/ / | | |/| | | | | | | | | | | CoqIDE does not have a "display" menu. It has a "view" menu with a list of display options.
* | / | | | | Warning about similar notations now up to alpha-conversion.Gravatar Hugo Herbelin2016-09-28
|/ / / / / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | Typeclass backtracking example by J. LeivantGravatar Matthieu Sozeau2016-09-28
| | | | | |
* | | | | | Remove incorrect assertion in cbn (bug #4822).Gravatar Guillaume Melquiond2016-09-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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).
* | | | | | Merge remote-tracking branch 'github/pr/232' into v8.6Gravatar Maxime Dénès2016-09-28
|\ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | Was PR#232: Fix the parsing of goal selectors.
* | | | | | | Fix bug #4553: CoqIDE gives warnings about deprecated GTK features.Gravatar Pierre-Marie Pédrot2016-09-27
| | | | | | |
* | | | | | | Fix #5061: Warnings flag has no discernible valueGravatar Maxime Dénès2016-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The default value of the warnings flag was printed as an empty string, now replaced by "default".
* | | | | | | Add fixed test-suite file for bug #4527Gravatar Matthieu Sozeau2016-09-27
| | | | | | |
| | * | | | | Fixing #4887 (confusion between using and with in documentation of firstorder).Gravatar Hugo Herbelin2016-09-27
| | | | | | |
* | | | | | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-27
|\ \ \ \ \ \ \ | | |/ / / / / | |/| | | | |
* | | | | | | LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)Gravatar Enrico Tassi2016-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | It seems we have no grammar rule that parses floats, so I'm parsing an integer, but the whole machinery supports floats.
* | | | | | | Remove spaces from around list notationsGravatar Jason Gross2016-09-26
| | | | | | |
* | | | | | | Remove spaces from around vector notationsGravatar Jason Gross2016-09-26
| | | | | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:54:34 +0000