| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-04-12 | Merge PR#441: Port Toplevel to the Stm API | Maxime Dénès | |
| 2017-04-12 | [flags] Documentation and a minor tweak. | Emilio Jesus Gallego Arias | |
| Mostly documentation and making a couple of local flags, local. | |||
| 2017-04-09 | Removing internal support for accepting "{struct x}" and co in "Theorem with". | Hugo Herbelin | |
| 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. | |||
| 2017-04-04 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-04-03 | Merge PR#417: No cast surgery in let in | Maxime Dénès | |
| 2017-04-02 | Fix higher-order pattern variables not being printed as "@?" (bug #5431). | Guillaume Melquiond | |
| 2017-03-30 | Merge PR#511: [stm] Remove some obsolete vernacs/classification. | Maxime Dénès | |
| 2017-03-27 | Do so that "About" tells if a reference is a coercion. | Hugo Herbelin | |
| 2017-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 2017-03-24 | [stm] Remove some obsolete vernacs/classification. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-03-24 | Applying same convention as in Definition for printing type in a let in. | Hugo Herbelin | |
| 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 *) | |||
| 2017-03-24 | Replacing "cast surgery" in LetIn by a proper field (see PR #404). | Hugo Herbelin | |
| 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. | |||
| 2017-03-24 | Unifying standard "constr_level" names for constructors of local_binder_expr. | Hugo Herbelin | |
| RawLocal -> CLocal | |||
| 2017-03-24 | Renaming local_binder into local_binder_expr. | Hugo Herbelin | |
| This is a bit long, but it is to keep a symmetry with constr_expr. | |||
| 2017-03-24 | "Standardizing" the name LocalPatten into LocalRawPattern. | Hugo Herbelin | |
| 2017-03-21 | [pp] Move terminal-specific tagging to the toplevel. | Emilio Jesus Gallego Arias | |
| Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`. | |||
| 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] 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-15 | Attempt 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-07 | Fixing Bug 5383 (Hyps Limit) + small refactoring. | Pierre Courtieu | |
| 2017-02-14 | Merge branch 'master'. | Pierre-Marie Pédrot | |
| 2017-02-14 | Namegen primitives now apply on evar constrs. | Pierre-Marie Pédrot | |
| Incidentally, this fixes a printing bug in output/inference.v where the displayed name of an evar was the wrong one because its type was not evar-expanded enough. | |||
| 2017-02-14 | Moving printing code from Evd to Termops. | Pierre-Marie Pédrot | |
| 2017-02-14 | Definining EConstr-based contexts. | Pierre-Marie Pédrot | |
| This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr. | |||
| 2017-02-14 | Introducing contexts parameterized by the inner term type. | Pierre-Marie Pédrot | |
| This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms. | |||
| 2017-02-14 | Evar-normalizing functions now act on EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing compatibility layers related to printing. | Pierre-Marie Pédrot | |
| 2017-02-14 | Ltac now uses evar-based constrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Removing some return type compatibility layers in Termops. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops now return EConstrs. | Pierre-Marie Pédrot | |
| 2017-02-14 | Tactic_matching API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Goal API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Reductionops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Termops API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-01 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2017-01-23 | Merge branch 'v8.5' into v8.6 | Pierre-Marie Pédrot | |
| 2017-01-05 | Fixing a little bug in printing cofix with no arguments. | Hugo Herbelin | |
| 2016-12-07 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-12-02 | Fixing printing of "ltac:" in tactics after surrounding parentheses | Hugo Herbelin | |
| became mandatory. | |||
| 2016-12-02 | Fixing printing of "Set Warnings Append". | Hugo Herbelin | |
| 2016-12-02 | Fixing space in printing "Context". | Hugo Herbelin | |
| 2016-12-02 | Fixing space in printing several list of implicit arguments. | Hugo Herbelin | |
| 2016-12-02 | Fixing printing of "only parsing" in abbreviations. | Hugo Herbelin | |
| 2016-12-02 | Protect printing of ltac's "context [...]" from possible collision | Hugo Herbelin | |
| with user-level notations by inserting spaces. | |||
| 2016-12-02 | More on fixing #5098 (preserving printing of "in hyp"). | Hugo Herbelin | |
| 2016-11-22 | Properly parenthesize "ltac:" arguments (bug #5169). | Guillaume Melquiond | |
| 2016-11-18 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-18 | Revert "Merge remote-tracking branch 'github/pr/360' into v8.6" | Maxime Dénès | |
| This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration. | |||
| 2016-11-17 | [stm] Remove STM-related vernaculars | Emilio Jesus Gallego Arias | |
| I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |