aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Revert "refactoring: Reductionops.contextual_reduction_function type"Gravatar Matej Košík2017-04-10
| | | | This reverts commit 470d0d56467a3a587dc34f958ffea8259618d1ae.
* Revert "comment: typo"Gravatar Matej Košík2017-04-10
| | | | This reverts commit cd248e01d6834bc43d733c08b5955c332d2146a6.
* Revert "refactoring: Names.DirPath.equal"Gravatar Matej Košík2017-04-10
| | | | This reverts commit 0d364f7aa5cee042f0b327966fce35778f3285e0.
* Revert "refactoring: Names.DirPath.compare"Gravatar Matej Košík2017-04-10
| | | | This reverts commit 7a51d6a94bdd6cc889cd69fa0fbb5c8a655b2b16.
* Revert "refactoring: Names.DirPath.is_empty"Gravatar Matej Košík2017-04-10
| | | | This reverts commit e180cce2384bacaa5ad5b9d6e15b55de8cc913cc.
* Revert "simplify: Environ.push_named"Gravatar Matej Košík2017-04-10
| | | | This reverts commit 9394aefa8e519a9e2b1b45659a47d5ff3f15ed16.
* Revert "trivial"Gravatar Matej Košík2017-04-10
| | | | This reverts commit 28973285f4b9389ed0610b94ba907684214dd279.
* Revert "trivial"Gravatar Matej Košík2017-04-10
| | | | This reverts commit 9b627431516f2cf88312329def9e0ec5e8605a98.
* Revert "comments: corrected in the Context module"Gravatar Matej Košík2017-04-10
| | | | This reverts commit 538d8edf708ba049e60e6bc32902ba5fdca720bb.
* comments: corrected in the Context moduleGravatar Matej Kosik2017-04-10
|
* trivialGravatar Matej Kosik2017-04-10
|
* trivialGravatar Matej Kosik2017-04-10
|
* simplify: Environ.push_namedGravatar Matej Kosik2017-04-10
|
* refactoring: Names.DirPath.is_emptyGravatar Matej Kosik2017-04-10
|
* refactoring: Names.DirPath.compareGravatar Matej Kosik2017-04-10
|
* refactoring: Names.DirPath.equalGravatar Matej Kosik2017-04-10
|
* comment: typoGravatar Matej Kosik2017-04-10
|
* refactoring: Reductionops.contextual_reduction_function typeGravatar Matej Kosik2017-04-10
|
* Merge PR#547: [toplevel] Remove the feedback printer only on exit.Gravatar Maxime Dénès2017-04-10
|\
* \ Merge PR#548: [ide] Correctly place warning tags.Gravatar Maxime Dénès2017-04-10
|\ \
* \ \ Merge PR#460: Turning the printing primitive projection compatibility flag ↵Gravatar Maxime Dénès2017-04-09
|\ \ \ | | | | | | | | | | | | off by default
| | * | [ide] Correctly place warning tags.Gravatar Emilio Jesus Gallego Arias2017-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.Gravatar Guillaume Melquiond2017-04-08
| | |
* | | Merge PR#461: [camlpX] Remove camlp4 compat layer.Gravatar Maxime Dénès2017-04-07
|\ \ \
| | | * [toplevel] Remove the feedback feeder printing only on exit.Gravatar Emilio Jesus Gallego Arias2017-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)Gravatar Matthieu Sozeau2017-04-07
| | |
* | | Merge PR#485: Document Show MatchGravatar Maxime Dénès2017-04-07
|\ \ \
* | | | Remove a forgotten rule for decl_mode from the Makefile.Gravatar Pierre-Marie Pédrot2017-04-07
| | | | | | | | | | | | | | | | This was making the miniopt target fail.
| | | * Turning the printing primitive projection parameter flag off by default.Gravatar Hugo Herbelin2017-04-07
| | | |
| | | * Turning the printing primitive projection compatibility flag off by default.Gravatar Hugo Herbelin2017-04-07
| |_|/ |/| |
| | * [travis] Overlay for PR#461: Camlp4 removal.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | |
| | * [camlpX] Enrico's changes to camlp4 removal.Gravatar Emilio Jesus Gallego Arias2017-04-07
| | | | | | | | | | | | | | | This removes some remaining support for camlp4 in the infrastructure and documents the change.
| | * [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-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 ↵Gravatar Maxime Dénès2017-04-07
|\ \ | | | | | | | | | printer.
* \ \ Merge PR#519: Faster side effectsGravatar Maxime Dénès2017-04-07
|\ \ \
| * | | Inline the only use of hcons_j in Term_typing.Gravatar Pierre-Marie Pédrot2017-04-07
| | | |
* | | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \ \
* \ \ \ \ Merge PR#488: Adding a documentation for the new proof engine.Gravatar Maxime Dénès2017-04-06
|\ \ \ \ \
| * | | | | Adding a documentation for the new proof engine.Gravatar Pierre-Marie Pédrot2017-04-06
|/ / / / /
| | * | | Documenting the fact terms are only hashconsed outside of a section.Gravatar Pierre-Marie Pédrot2017-04-06
| | | | |
* | | | | Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR#542: [travis] Add webhook to Gitter.Gravatar Maxime Dénès2017-04-06
|\ \ \ \ \ \
| * | | | | | [travis] Add webhook to Gitter.Gravatar Théo Zimmermann2017-04-06
| | | | | | |
| | | | | * | [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-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.Gravatar Maxime Dénès2017-04-05
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#502: [pp] Add anomaly header to error messages.Gravatar Maxime Dénès2017-04-04
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-03
|\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge PR#533: Instances should obey universe binders even when defined by ↵Gravatar Maxime Dénès2017-04-03
| |\ \ \ \ \ \ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | tactics.
* | | | | | | | | | Fix loading of ocamldebug printers.Gravatar Pierre-Marie Pédrot2017-04-03
| | | | | | | | | |
| | * | | | | | | | Instances should obey universe binders even when defined by tactics.Gravatar Gaetan Gilbert2017-04-03
| |/ / / / / / / /
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 16:53:50 +0000