| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-07-19 | Merge PR #770: [proof] Move bullets to their own module. | Maxime Dénès | |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot | |
| 2017-06-25 | Moving "assert" (internally "Cut") to the new proof engine. | Hugo Herbelin | |
| It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>". | |||
| 2017-06-16 | Clean up universes of constants and inductives | Amin Timany | |
| 2017-06-16 | Add printing of cumulativity in inductive types | Amin Timany | |
| 2017-06-16 | Using UInfoInd for universes in inductive types | Amin Timany | |
| It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. | |||
| 2017-06-12 | [proof] Move bullets to their own module. | Emilio Jesus Gallego Arias | |
| Bullets were placed inside the `Proof_global` module, I guess that due to the global registration function. However, it has logically nothing to do with the functionality of `Proof_global` and the current placement may create some interference between the developers reworking proof state handling and bullets. We thus put the bullet functionality into its own, independent file. | |||
| 2017-06-11 | [proof] Deprecate redundant wrappers. | Emilio Jesus Gallego Arias | |
| As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`. | |||
| 2017-06-01 | [emacs] [toplevel] Make emacs flag local to the toplevel. | Emilio Jesus Gallego Arias | |
| We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel. | |||
| 2017-05-27 | [cleanup] Unify all calls to the error function. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-05-25 | Merge PR#481: [option] Remove support for non-synchronous options. | Maxime Dénès | |
| 2017-05-24 | Merge branch 'trunk' into located_switch | Emilio Jesus Gallego Arias | |
| 2017-05-24 | [option] Remove support for non-synchronous options. | Emilio Jesus Gallego Arias | |
| 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. | |||
| 2017-05-17 | Merge PR#457: Adding an even more compact goal hyps mode. | Maxime Dénès | |
| 2017-05-16 | Simplified compaction criterion + tests. | Pierre Courtieu | |
| 2017-05-05 | Adapted to EConstr. | Pierre Courtieu | |
| 2017-05-04 | Warning removed. | Pierre Courtieu | |
| 2017-05-04 | labelizing arguments | Pierre Courtieu | |
| 2017-05-04 | Adding an option "Printing Unfocused". | Pierre Courtieu | |
| Off by default. + small refactoring of emacs hacks in printer.ml. | |||
| 2017-05-03 | Adding an even more compact mode for goal display. | Pierre Courtieu | |
| 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). | |||
| 2017-04-27 | Remove some unused values and types | Gaetan Gilbert | |
| 2017-04-25 | [location] Remove Loc.ghost. | Emilio Jesus Gallego Arias | |
| Now it is a private field, locations are optional. | |||
| 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-03-24 | Merge branch 'trunk' into pr379 | Maxime Dénès | |
| 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-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 | 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 | Tactic_matching API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Goal API using EConstr. | Pierre-Marie Pédrot | |
| 2017-02-14 | Termops API using EConstr. | Pierre-Marie Pédrot | |
| 2016-11-18 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-11-05 | Do not print dependent evars by default (expensive) | Matthieu Sozeau | |
| The option can be turned on by the user though. | |||
| 2016-10-24 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-10-20 | Refine printing of pending unification constraints | Matthieu Sozeau | |
| It now prints evars with candidates as well if there are any. | |||
| 2016-09-27 | Merge branch 'v8.6' | Pierre-Marie Pédrot | |
| 2016-09-24 | Moving "move" in the new proof engine. | Hugo Herbelin | |
| 2016-08-26 | CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, ↵ | Matej Kosik | |
| which can be useful in general, and then simplifying "Printer.pr_named_decl" function | |||
| 2016-08-26 | CLEANUP: renaming "Printer.pr_var_decl" function to "Printer.pr_named_decl" | Matej Kosik | |
| 2016-08-26 | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted" | Matej Kosik | |
| 2016-08-25 | CLEANUP: changing the definition of the "Context.NamedList.Declaration" type | Matej Kosik | |
| 2016-08-24 | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function | Matej Kosik | |
| 2016-07-03 | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵ | Pierre Letouzey | |
| module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a | |||
| 2016-06-19 | Add [Unset Printing Dependent Evars Line] | Jason Gross | |
| This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |