Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | refactoring: Reductionops.contextual_reduction_function type | 2017-04-10 | |
| | |||
* | Merge PR#547: [toplevel] Remove the feedback printer only on exit. | 2017-04-10 | |
|\ | |||
* \ | Merge PR#548: [ide] Correctly place warning tags. | 2017-04-10 | |
|\ \ | |||
* \ \ | Merge PR#460: Turning the printing primitive projection compatibility flag ↵ | 2017-04-09 | |
|\ \ \ | | | | | | | | | | | | | off by default | ||
| | * | | [ide] Correctly place warning tags. | 2017-04-08 | |
| |/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 8e07227c5853de78eaed4577eefe908fb84507c0 introduced an incorrect duplicate of `position_error_tag_at_sentence`, which sets the end of the underlining position starting at the end of the sentence, whereas the location in the feedback refers to the beginning, thus it highlights more text than it should. This was missed in 8.6 as it seems that the code was not called. We undo the duplication and fix the bug. | ||
* | | | Update the .mailmap file. | 2017-04-08 | |
| | | | |||
* | | | Merge PR#461: [camlpX] Remove camlp4 compat layer. | 2017-04-07 | |
|\ \ \ | |||
| | | * | [toplevel] Remove the feedback feeder printing only on exit. | 2017-04-07 | |
| |_|/ |/| | | | | | | | | | | | | | | This fixes the bug in `Drop` reported by @mattam82: after performing a `Drop`, the feeder was lost and no further message from Coq was printed. | ||
* | | | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac) | 2017-04-07 | |
| | | | |||
* | | | Merge PR#485: Document Show Match | 2017-04-07 | |
|\ \ \ | |||
* | | | | Remove a forgotten rule for decl_mode from the Makefile. | 2017-04-07 | |
| | | | | | | | | | | | | | | | | This was making the miniopt target fail. | ||
| | | * | Turning the printing primitive projection parameter flag off by default. | 2017-04-07 | |
| | | | | |||
| | | * | Turning the printing primitive projection compatibility flag off by default. | 2017-04-07 | |
| |_|/ |/| | | |||
| | * | [travis] Overlay for PR#461: Camlp4 removal. | 2017-04-07 | |
| | | | |||
| | * | [camlpX] Enrico's changes to camlp4 removal. | 2017-04-07 | |
| | | | | | | | | | | | | | | | This removes some remaining support for camlp4 in the infrastructure and documents the change. | ||
| | * | [camlpX] Remove camlp4 compat layer. | 2017-04-07 | |
| |/ |/| | | | | | | | | | | | | | We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes. | ||
* | | Merge PR#530: [toplevel] Remove exception error printer in favor of feedback ↵ | 2017-04-07 | |
|\ \ | | | | | | | | | | printer. | ||
* \ \ | Merge PR#519: Faster side effects | 2017-04-07 | |
|\ \ \ | |||
| * | | | Inline the only use of hcons_j in Term_typing. | 2017-04-07 | |
| | | | | |||
* | | | | Merge PR#455: Farewell decl_mode | 2017-04-06 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR#488: Adding a documentation for the new proof engine. | 2017-04-06 | |
|\ \ \ \ \ | |||
| * | | | | | Adding a documentation for the new proof engine. | 2017-04-06 | |
|/ / / / / | |||
| | * | | | Documenting the fact terms are only hashconsed outside of a section. | 2017-04-06 | |
| | | | | | |||
* | | | | | Merge PR#508: Optimize pending evars | 2017-04-06 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#542: [travis] Add webhook to Gitter. | 2017-04-06 | |
|\ \ \ \ \ \ | |||
| * | | | | | | [travis] Add webhook to Gitter. | 2017-04-06 | |
| | | | | | | | |||
| | | | | * | | [toplevel] Remove exception error printer in favor of feedback printer. | 2017-04-05 | |
| |_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429 | ||
* | | | | | | Merge PR#434: Optimizing array mapping in the kernel. | 2017-04-05 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR#502: [pp] Add anomaly header to error messages. | 2017-04-04 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | 2017-04-03 | |
|\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR#533: Instances should obey universe binders even when defined by ↵ | 2017-04-03 | |
| |\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | tactics. | ||
* | | | | | | | | | | Fix loading of ocamldebug printers. | 2017-04-03 | |
| | | | | | | | | | | |||
| | * | | | | | | | | Instances should obey universe binders even when defined by tactics. | 2017-04-03 | |
| |/ / / / / / / / | |||
* | | | | | | | | | Merge PR#417: No cast surgery in let in | 2017-04-03 | |
|\ \ \ \ \ \ \ \ \ | |||
| | * | | | | | | | | Add test file for #4957. | 2017-04-03 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Bug #4957 was "unify cannot directly unify universes with evars, but can do so indirectly". | ||
* | | | | | | | | | | Fix higher-order pattern variables not being printed as "@?" (bug #5431). | 2017-04-02 | |
| | | | | | | | | | | |||
* | | | | | | | | | | Fix documentation typo (bug #5433). | 2017-04-02 | |
| | | | | | | | | | | |||
* | | | | | | | | | | Simplify some proofs. | 2017-04-02 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit does not modify the signature of the involved modules, only the opaque proof terms. One has to wonder how proofs can bitrot so much that several occurrences of "replace 4 with 4" start appearing. | ||
* | | | | | | | | | | Declaring ltac plugin, so that static linking works. | 2017-04-01 | |
| | | | | | | | | | | |||
* | | | | | | | | | | Merge branch 'v8.6' into trunk | 2017-03-30 | |
|\ \ \ \ \ \ \ \ \ \ | | |/ / / / / / / / | |/| | | | | | | | | |||
| * | | | | | | | | | Merge PR#463: Run non-tactic comands without resilient_command | 2017-03-30 | |
| |\ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | 2017-03-30 | |
| | | | | | | | | | | | |||
* | | | | | | | | | | | Merge PR#469: Added take to VectorDef | 2017-03-30 | |
|\ \ \ \ \ \ \ \ \ \ \ | |||
| * | | | | | | | | | | | Added take to VectorDef. | 2017-03-30 | |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Added a function that takes the first [p] elements of a vector, and a few lemmas proving some of its properties. | ||
* | | | | | | | | | | | | Merge PR#511: [stm] Remove some obsolete vernacs/classification. | 2017-03-30 | |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#522: [coqide] Protect against size_allocate race in proofview. | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | | |_|_|/ / / / / / / / / / | |/| | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | Merge PR#514: [travis] Backport from trunk: VST | 2017-03-29 | |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* | \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#506: [nit] Fix a couple incorrect uses of msg_error. | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#521: Do so that "About" tells if a reference is a coercion. | 2017-03-29 | |
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |