aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2017-03-21[feedback] Allow to remove feedback listeners.Emilio Jesus Gallego Arias
2017-03-21[pp] Remove redundant white spacing pp construct.Emilio Jesus Gallego Arias
2017-03-21[pp] Force well-formed boxes by construction.Emilio Jesus Gallego Arias
We replace open/close box commands in favor of the create box ones.
2017-03-21[pp] Force well-tagged docs by construction.Emilio Jesus Gallego Arias
We replace open/close tag commands by a well-balanced "tag" wrapper.
2017-03-21[pp] Implement n-ary glue.Emilio Jesus Gallego Arias
2017-03-21[pp] Make pp public to allow serialization.Emilio Jesus Gallego Arias
2017-03-21[pp] Prepare for serialization, remove opaque glue.Emilio Jesus Gallego Arias
We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter.
2017-03-21[pp] Remove `Pp.stras`.Emilio Jesus Gallego Arias
Mostly unused, we ought to limit spacing in the boxes themselves.
2017-03-21[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`Emilio Jesus Gallego Arias
This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags.
2017-03-21[pp] Remove unused printing tagging infrastructure.Emilio Jesus Gallego Arias
Applications of it were not clear/unproven, it made printers more complex (as they needed to be functors) and as it lacked examples it confused some people. The printers now tag unconditionally, it is up to the backends to interpreted the tags. Tagging (and indeed the notion of rich document) should be reworked in a follow-up patch, so they are in sync, but this is a first step. Tested, test-suite passes. Notes: - We remove the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in sync). - Note that Richpp didn't need a single change. In particular, its main API entry point `Richpp.rich_pp` is not used by anyone.
2017-03-21[ide] ide_slave doesnt't need to capture stdoutEmilio Jesus Gallego Arias
The miscellaneous `msg_*` cleanup patches have finally enforced this invariant.
2017-03-21[ide] Use "log via feedback".Emilio Jesus Gallego Arias
We remove the custom logger handler in ide_slave, and handle everything via feedback. This is an experimental patch but it seems to bring quite a bit of cleanup and a more uniform handling to messaging.
2017-03-21Merge PR#134: Enable `-safe-string`Maxime Dénès
2017-03-21trivial: fix commentMatej Kosik
2017-03-20[misc] Remove warnings about String.setEmilio Jesus Gallego Arias
The `a.[i] <- x` notation is deprecated and we were getting a couple of warnings.
2017-03-20Merge PR#479: [future] Remove unused parameter greedy.Maxime Dénès
2017-03-19Merge PR#487: Add a forgotten (?) line to "theories/Logic/vo.itarget".Maxime Dénès
2017-03-19Add a forgotten (?) line to "theories/Logic/vo.itarget".Matej Kosik
The "theories/Logic/PropExtensionalityFacts.v" file was: - compiled - used in several places but not actually installed. This commit fixes that.
2017-03-17Merge PR#428: Report missing tactic arguments in error messageMaxime Dénès
2017-03-17Merge PR#437: Improve unification debug trace.Maxime Dénès
2017-03-17Merge PR#445: TACTIC EXTEND now takes an optional level as argument.Maxime Dénès
2017-03-17Merge PR#442: Allow interactive editing of Coq.Init.LogicMaxime Dénès
2017-03-17Merge PR#451: Add η principles for sigma typesMaxime Dénès
2017-03-15Attempt to improve error message when "apply in" fail.Hugo Herbelin
- Adding a better location in the "apply" on the fly pattern. - Printing statement of lemma and of hypothesis. Was suggested by discussion at wish report #5390.
2017-03-15Merge PR#267: Proposal for an update of the recommended style in programming ↵Maxime Dénès
Coq.
2017-03-14[safe-string] Enable -safe-string !Emilio Jesus Gallego Arias
We now build Coq with `-safe-string`, which enforces functional use of the `string` datatype. Coq was pretty safe in these regard so only a few tweaks were needed. - coq_makefile: build plugins with -safe-string too. - `names.ml`: we remove `String.copy` uses, as they are not needed.
2017-03-14[safe-string] toolsEmilio Jesus Gallego Arias
No functional changes.
2017-03-14[safe-string] ideEmilio Jesus Gallego Arias
No functional change, one extra copy introduced but it seems hard to avoid.
2017-03-14[safe-string] plugins/extractionEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe-string] ltac/profile_ltacEmilio Jesus Gallego Arias
No functional change, one extra copy introduced but it seems hard to avoid.
2017-03-14[safe_string] toplevel/vernacEmilio Jesus Gallego Arias
No functional changes, only a minor copy on a deprecated output option.
2017-03-14[safe_string] toplevel/coqloopEmilio Jesus Gallego Arias
No functional change, even if we could optimize `blanch_utf8_string` a bit more by using `String.init`.
2017-03-14[safe-string] parsing/cLexerEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] interp/dumpglobEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] library/nameopsEmilio Jesus Gallego Arias
We add a more convenient API to create identifiers from mutable strings. We cannot solve the `String.copy` deprecation problem until we enable `-safe-string`.
2017-03-14[safe_string] kernel/cemitcodesEmilio Jesus Gallego Arias
The `emitcodes` string type was used in both a functional and an imperative way, so we have to handle it with care in order to preserve the previous optimizations and semantics.
2017-03-14Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoMaxime Dénès
2017-03-14Report missing tactic arguments in error messageTej Chajed
Augments "A fully applied tactic is expected" with the list of missing arguments to the tactic. Addresses [bug 5344](https://coq.inria.fr/bugs/show_bug.cgi?id=5344).
2017-03-14[safe-string] kernel/nativevaluesEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] kernel/term_typingEmilio Jesus Gallego Arias
No functional change, we create the new string beforehand and `id_of_string` will become a noop with `-safe-string`.
2017-03-14[safe-string] lib/miscelaneaEmilio Jesus Gallego Arias
No functional change.js
2017-03-14[safe-string] lib/cUnixEmilio Jesus Gallego Arias
No functional change.
2017-03-14[safe_string] lib/cThreadEmilio Jesus Gallego Arias
No functional changes.
2017-03-14Merge PR#438: Fix V7 syntax in refman.Maxime Dénès
2017-03-14Merge PR#412: Remove outdated comment from 2002.Maxime Dénès
2017-03-14Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFunMaxime Dénès
2017-03-14Merge PR#477: [travis] Basic support for overlays.Maxime Dénès
2017-03-14Merge PR#473: [ci] Document that sudo: false is slowerMaxime Dénès
2017-03-14Merge PR#464: [META] More fixesMaxime Dénès
2017-03-14Merge PR#446: Remove a dead exception catching code.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 20:09:50 +0000