aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing
Commit message (Collapse)AuthorAge
* Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\
* \ Merge PR#722: [printing] Remove duplicated printing function.Gravatar Maxime Dénès2017-06-05
|\ \
| | * Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
| | * Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
| |/ |/| | | | | | | | | | | | | We don't want "Anomaly: Returned a functional value in a type not recognized as a product type.. Please report at http://coq.inria.fr/bugs/." but instead "Anomaly: Returned a functional value in a type not recognized as a product type. Please report at http://coq.inria.fr/bugs/."
* | Merge PR#647: [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Maxime Dénès2017-06-02
|\ \
| * | [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
| | | | | | | | | | | | | | | We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel.
| | * [printing] Remove duplicated printing function.Gravatar Emilio Jesus Gallego Arias2017-06-01
| |/ | | | | | | It seems there were 4 copies of the same function in the code base.
* / Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
|/ | | | | | | | | | | | This module collects the functions of Nameops which are about Name.t and somehow standardize or improve their name, resulting in particular from discussions in working group. Note the use of a dedicated exception rather than a failwith for Nameops.Name.out. Drawback of the approach: one needs to open Nameops, or to use long prefix Nameops.Name.
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| | * [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| * | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We'd like to cleanup the `proof_end` type so we can have a smaller path in proof save. Note that the construction: ``` Goal Type. ⋮ Save id. ``` has to be handled by the STM in the same path as Defined (but with an opaque flag), as `Save id` will alter the environment and cannot be processed in parallel. We thus try to simply such paths a bit, as complexity of `lemmas.ml` seems like an issue these days. The form `Save Theorem id` doesn't really seem used, and moreover we should really add a type of "Goal", and unify syntax. It is often the case that beginners try `Goal addnC n : n + 0 = n." etc...
| * Merge PR#457: Adding an even more compact goal hyps mode.Gravatar Maxime Dénès2017-05-17
| |\
| | * Simplified compaction criterion + tests.Gravatar Pierre Courtieu2017-05-16
| | |
| * | Merge PR#454: Printing unfocussed goals and toward a pg plugin.Gravatar Maxime Dénès2017-05-05
| |\ \
| | | * Adapted to EConstr.Gravatar Pierre Courtieu2017-05-05
| | | |
| | * | Warning removed.Gravatar Pierre Courtieu2017-05-04
| | | |
| | * | labelizing argumentsGravatar Pierre Courtieu2017-05-04
| | | |
| | * | Adding an option "Printing Unfocused".Gravatar Pierre Courtieu2017-05-04
| | | | | | | | | | | | | | | | | | | | | | | | Off by default. + small refactoring of emacs hacks in printer.ml.
| | | * Adding an even more compact mode for goal display.Gravatar Pierre Courtieu2017-05-03
| | |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We want to print variables in vertical boxes as much as possible. The criterion to distinguish "variable" from "hypothesis" is not obvious. We chose this one but may change it in the future: X:T is a variable if T is not of type Prop AND T is "simple" which means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall Ti:Type, but not Ti:nat).
| * / Allow flexible anonymous universes in instances and sorts.Gravatar Gaetan Gilbert2017-05-03
| |/ | | | | | | The addition to the test suite showcases the usage.
| * Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\
| * \ Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Gravatar Maxime Dénès2017-04-28
| |\ \ | | | | | | | | | | | | let-ins
| | | * Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
| | | |
| | | * Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| | | |
| | | * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | |/ | |/|
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
| | |
* | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes.
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | Now it is a private field, locations are optional.
* | | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | |
* | | [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | |
* | | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location.
* | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is first of a series of patches, converting `constrexpr` pattern data type from ad-hoc location handling to `Loc.located`. Along Coq, we can find two different coding styles for handling objects with location information: one style uses `'a Loc.located`, whereas other data structures directly embed `Loc.t` in their constructors. Handling all located objects uniformly would be very convenient, and would allow optimizing certain cases, in particular making located smarter when there is no location information, as it is the case for all terms coming from the kernel. `git grep 'Loc.t \*'` gives an overview of the remaining work to do. We've also added an experimental API for `located` to the `Loc` module, `Loc.tag` should be used to add locations objects, making it explicit in the code when a "located" object is created.
* | Merge PR#552: Miscelaneous commitsGravatar Maxime Dénès2017-04-24
|\ \
* | | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| | |
| * | refactoring "Ppvernac.pr_extend"Gravatar Matej Kosik2017-04-20
|/ /
* | Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \
| * | [flags] Documentation and a minor tweak.Gravatar Emilio Jesus Gallego Arias2017-04-12
| | | | | | | | | | | | Mostly documentation and making a couple of local flags, local.
| | * Removing internal support for accepting "{struct x}" and co in "Theorem with".Gravatar Hugo Herbelin2017-04-09
| |/ | | | | | | | | There were actually no syntax for it, and I'm still unsure what good syntax to give to it, even more that it would be useful to have one.
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\|
| * Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
| |\
| * | Fix higher-order pattern variables not being printed as "@?" (bug #5431).Gravatar Guillaume Melquiond2017-04-02
| | |
| * | Merge PR#511: [stm] Remove some obsolete vernacs/classification.Gravatar Maxime Dénès2017-03-30
| |\ \
| * | | Do so that "About" tells if a reference is a coercion.Gravatar Hugo Herbelin2017-03-27
| | | |
* | | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\| | |
| | * | [stm] Remove some obsolete vernacs/classification.Gravatar Emilio Jesus Gallego Arias2017-03-24
| |/ / | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away.
| | * Applying same convention as in Definition for printing type in a let in.Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | Also adding spaces around ":=" and ":" when printed as "(x : t := c)". Example: Check fun y => let x : True := I in fun z => z+y=0. (* λ (y : nat) (x : True := I) (z : nat), z + y = 0 : nat → nat → Prop *)
| | * Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information.