aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-09-30Give name to warning added in (fdfcdc): arguments-ignore-rename-nonimplEnrico Tassi
2016-09-30Merge remote-tracking branch 'github/pr/294' into v8.5Maxime Dénès
Was PR#294: Make error message more helpful.
2016-09-30Merge remote-tracking branch 'github/pr/257' into v8.6Maxime Dénès
Was PR#257: [checker] Fix/fine tune printing.
2016-09-30Merge branch 'v8.5' into v8.6Maxime Dénès
2016-09-30[pp] Remove duplicate color logger.Emilio Jesus Gallego Arias
We use the same printing path for color and mono terminal output, thus removing the duplicate printers which avoids problems as they don't have to be kept in sync anymore. We tag unconditionally but set the `pp_tag` tagger properly. This removes IO from `Ppstyle` with IMO is the right thing to do. Test suite passes.
2016-09-30Merge branch '4762' into v8.5Maxime Dénès
Was PR#293: Fix #4762 (eauto weaker than auto).
2016-09-30Fix #4762.Cyprien Mangin
2016-09-29LtacProf cutoff is for total percent, not timeJason Gross
2016-09-29Set 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-29Move vector/list compat notations to their relevant filesJason Gross
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
2016-09-29Fix 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-29STM: 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-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
It seems warnings are not taken into account in output/ tests.
2016-09-29Merge branch 'bug5036' into v8.6Matthieu Sozeau
2016-09-29Fix bug #5036 autorewrite, sections and universesMatthieu 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-29Merge branch 'bug4723' into v8.6Matthieu Sozeau
2016-09-29Fix bug 4969, autoapply was not tagging shelved subgoals correctly as ↵Matthieu Sozeau
unresolvable
2016-09-29Being more informative about the change of behavior of "subst".Hugo Herbelin
2016-09-29Fix bug #4869, allow Prop, Set, and level names in constraints.Matthieu Sozeau
2016-09-29fix bug 3683 : adds references to the web site for the bug trackerYves Bertot
in error messages
2016-09-29Fix bug #5011: Anomaly on [Existing Class].Pierre-Marie Pédrot
2016-09-29Fix a bug in subst releaved by an OCaml warning.Maxime Dénès
2016-09-29test-suite: fix sed on OS X, does not handle +Matthieu Sozeau
2016-09-29Cleanup API, making inference_hook optionalMatthieu Sozeau
2016-09-29Ncring_initial: avoid a notation overridingPierre Letouzey
2016-09-29Extraction: ignore some useless stuff about universesPierre Letouzey
2016-09-29Argument : 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-29Updating the code wrt. to some Ocaml compiler warnings.Matej Kosik
2016-09-29UPDATE: reference to a deprecated variable "Filename.temp_dir_name" was ↵Matej Kosik
replaced with the recommended "Filename.get_temp_dir_name".
2016-09-28Ring_theory: avoid overriding a few notationsPierre Letouzey
2016-09-28ZDivEucl: notations in different scope to avoid a warningPierre Letouzey
2016-09-28Adding interface files to Nsatz ML files.Pierre-Marie Pédrot
2016-09-28Fix bug #4723 and FIXME in API for solve_by_tacMatthieu 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-28Do 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-28Make 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-28CLEANUP: remove the definition of the "CString.map" function. We will use ↵Matej Kosik
the official "String.map" function instead.
2016-09-28FIX: a bug in the pattern matchingMatej Kosik
2016-09-288.7 now points to Current and 8.6 points to V8_6.Théo Zimmermann
2016-09-28Add a compatibility flag for 8.6 and refactor.Théo Zimmermann
2016-09-28Warning 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-28Typeclass backtracking example by J. LeivantMatthieu Sozeau
2016-09-28Remove 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-28Merge remote-tracking branch 'github/pr/232' into v8.6Maxime Dénès
Was PR#232: Fix the parsing of goal selectors.
2016-09-27Fix bug #4553: CoqIDE gives warnings about deprecated GTK features.Pierre-Marie Pédrot
2016-09-27Fix #5061: Warnings flag has no discernible valueMaxime Dénès
The default value of the warnings flag was printed as an empty string, now replaced by "default".
2016-09-27Add fixed test-suite file for bug #4527Matthieu Sozeau
2016-09-27Fixing #4887 (confusion between using and with in documentation of firstorder).Hugo Herbelin
2016-09-27Merge remote-tracking branch 'github/pr/290' into trunkMaxime Dénès
Was PR#290: Add a compatibility flag for 8.6 and refactor.
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 04:17:53 +0000