aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-10-05Merge PR #1101: Fixing an old proof engine bug in collecting evars with ↵Maxime Dénès
cleared context.
2017-10-05Merge PR #1059: coq_makefile: make sure compile flags for Coq and ↵Maxime Dénès
coq_makefile are in sync (supersed #1039)…
2017-10-05Merge PR #1112: Fix GeoCoq CI and remove it from allowed failuresMaxime Dénès
2017-10-04Merge PR #1006: fix: ssrmatching and primitive projectionsMaxime Dénès
2017-10-04Merge PR #1078: Report missing arguments in error messageMaxime Dénès
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-03fix compilation on OCaml < 4.04Enrico Tassi
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-03Remove GeoCoq from allowed failures.Théo Zimmermann
2017-10-03Fix GeoCoq build by using a shared CI configure.Théo Zimmermann
See also GeoCoq/GeoCoq#7.
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-27Fixing an old bug in collecting evars with cleared context.Hugo Herbelin
The function Proofview.undefined was collecting twice the evars that had advanced. Consequently, the functions Proofview.unshelve and Proofview.with_shelf were possibly doing the same.
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 04:05:19 +0000