aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-04Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]Maxime Dénès
2017-10-04Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Maxime Dénès
2017-10-03Merge PR #1110: Mention requiring extraction/funind in CHANGESMaxime Dénès
2017-10-03Merge PR #1105: [stm] Remove unused "Proof using" data in `Sync` tags.Maxime Dénès
2017-10-03Merge PR #1104: Browser userscript to turn BZ#XXXX occurences into links.Maxime Dénès
2017-10-03Merge PR #1100: Avoid looping when searching for CoqProject.Maxime Dénès
2017-10-03Merge PR #1099: BZ#5637, look for Obligation num or Next Obligation to start ↵Maxime Dénès
proof for coqwc
2017-10-03Merge PR #1097: Properly display the "only" prefix for selectors (bug #5760).Maxime Dénès
2017-10-03Merge PR #1094: Fixing a little parsing bug with level 90 introduced in ↵Maxime Dénès
3e70ea9c.
2017-10-03Merge PR #1090: [ide] Avoid duplicate error printing (BZ#5583)Maxime Dénès
2017-10-03Merge PR #1084: After testing it in live, writing metas using an ↵Maxime Dénès
?INTERNAL#42 style is ugly
2017-10-03Merge PR #1015: Adding a function to be typically used to pass values from ↵Maxime Dénès
an OCaml "when" clause to the r.h.s of the matching clause
2017-10-03Merge PR #1080: Remove some unused parts of the reference manual.Maxime Dénès
2017-10-03Merge PR #1076: Properly handle "coq_makefile -Q . Foo" (bug #5580).Maxime Dénès
2017-10-03Merge PR #1072: Do not run Travis OS X packaging job on PRsMaxime Dénès
2017-10-03Merge PR #1040: Efficient fresh name generationMaxime Dénès
2017-10-03Merge PR #1023: dev/build/windows/makecoq_mingw.sh: install camlp5's META fileMaxime Dénès
2017-10-03Merge PR #1019: Fix BZ#5655 by avoiding the creation of a cleaner thread for ↵Maxime Dénès
empty queues.
2017-10-03Merge PR #1012: Make a test for coq_makefile portable.Maxime Dénès
2017-10-03Merge PR #667: [vernac] Remove `Qed exporting` syntax.Maxime Dénès
2017-10-02Mention requiring extraction/funind in CHANGESTej Chajed
2017-09-29[ide] Avoid duplicate error printing (BZ#5583)Emilio Jesus Gallego Arias
See the discussion in the bug tracker, basically the STM delays the feedback error message to a point where CoqIDE has forgotten about the sentence, thus we were processing such errors in the generic case, printing them twice as the Fail case will also do it. We could indeed revert back to the 8.6 strategy for error (print always from Fail and ignore Feedback), however I feel that time will be better spent by fixing the STM than adding more CoqIDE workarounds.
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-28Efficient fresh name generation relying on sets.Pierre-Marie Pédrot
The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n).
2017-09-27[stm] Warn about costly Undo operations in batch mode [BZ#5677]Emilio Jesus Gallego Arias
Undo & friends is very expensive in batch mode as backtracking state is not kept and thus should be recomputed. We thus warn the user.
2017-09-27[stm] Remove unused "Proof using" data in `Sync` tags.Emilio Jesus Gallego Arias
This was not used anywhere; it looks like dead code from some previous attempt. `get_hint_ctx` looks also very very suspicious.
2017-09-27Browser userscript to turn BZ#XXXX occurences into links.Gaëtan Gilbert
2017-09-27Avoid looping when searching for CoqProject.Maxime Dénès
This could happen with paths on Windows, or even relative paths on all OSs. Fixes #5730: CoqIDE becomes unresponsive on file open.
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-26look for Obligation num or Next Obligation to start proofPaul Steckler
2017-09-26Properly display the "only" prefix for selectors (bug #5760).Guillaume Melquiond
This commit also fixes range selectors being incorrectly displayed.
2017-09-25Fixing a little parsing bug with level 90 introduced in 3e70ea9c.Hugo Herbelin
Unfortunately, some manual synchronization is needed between the constr parser and the table of constr/pattern levels. We do this synchronization which was missing in the commit moving "x -> y" to a user-level notation.
2017-09-25Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ↵Maxime Dénès
inductive types)
2017-09-25Merge PR #1083: Fixing bug in building _rect scheme for inductive types with ↵Maxime Dénès
let-ins and non-recursively uniform parameters
2017-09-25Merge PR #1079: Avoid generated names for html pages of the reference manual ↵Maxime Dénès
(bug #4742).
2017-09-25Merge PR #1068: Fixing #5749 (bug in fold_constr_with_binders introduced in ↵Maxime Dénès
4e70791).
2017-09-25Merge PR #1057: Reporting locations in error messages about notation formats.Maxime Dénès
2017-09-25Merge PR #1060: An optimization of tactic constructorMaxime Dénès
2017-09-25Merge PR #1075: Re-enable checker error messagesMaxime Dénès
2017-09-23Discharge.ml: cosmetic renaming of some variables.Hugo Herbelin
The point is to emphasize stronglier when we are talking about contexts or about arguments.
2017-09-23Fixing #5755 (discharging of inductive types not correct with let-ins).Hugo Herbelin
The number of effective parameters was used where the number of declarations in the signature of parameters should have been used.
2017-09-23After testing it in live, writing metas using an ?INTERNAL#42 style is ugly.Hugo Herbelin
Printing metas still happens relatively often. From the user point of view, no need to know that it is different from an evar, so the notation ?M42 as it was before is much lighter. As for developers looking for debugging information, they will easily suspect that it is internally a meta because of the "M". This reverts "Proposing meta names more distinguishable from evar names than ?M42." (dc5b8f1793c6f7104f0b4762d9887be255709ead).
2017-09-23Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).Hugo Herbelin
2017-09-23Fixing _rect bug for inductive types with let-ins and non-rec uniform params.Hugo Herbelin
The bug was caused by an inconsistency in different part of the code for deciding where cutting the context in between recursively uniform parameters and non-recursively uniform ones when let-ins were in the middle. We fix it by using uniformly "context_chop".
2017-09-22Remove some unused parts of the reference manual.Guillaume Melquiond
2017-09-22Avoid generated names for html pages of the reference manual (bug #4742).Guillaume Melquiond
2017-09-22Make a test for coq_makefile portable.Pierre-Marie Pédrot
The validity of this test depended on Makefile issueing warnings in English. We simply force the global language of the shell to be C.
2017-09-22Merge PR #1055: Remove STM vernacularsMaxime Dénès
2017-09-22Merge PR #1065: In gitlab set TRAVIS_BRANCH so user overlays will work as ↵Maxime Dénès
expected.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 05:02:02 +0000