| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-11-20 | Merge PR #7925: Clean transparent state | Maxime Dénès | |
| 2018-11-19 | [pfedit] Remove `start_proof` stub from `Pfedit` | Emilio Jesus Gallego Arias | |
| This way we only have 2 `start_proof` entries, in `Lemmas` and `Proof_global`; which they should be unified / brought closer in the future. | |||
| 2018-11-19 | Merge PR #8987: Deprecate hint declaration/removal with no specified database | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #9003: [vernacextend] Consolidate extension points API | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8894: Print full binders in subtyping incompatible polymorphism error. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #9001: [options] Remove deprecated option automatic introduction. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8999: [pfedit] Remove cook_proof stub. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #9023: [gramlib] Remove unused alias. | Pierre-Marie Pédrot | |
| 2018-11-19 | Rename TranspState into TransparentState. | Pierre-Marie Pédrot | |
| 2018-11-19 | Proper record type and accessors for transparent states. | Pierre-Marie Pédrot | |
| This is documented in dev/doc/changes.md. | |||
| 2018-11-19 | Move transparent_state to its own module. | Pierre-Marie Pédrot | |
| 2018-11-19 | Merge PR #8451: Print Universes Subgraph | Pierre-Marie Pédrot | |
| 2018-11-19 | [gramlib] Remove unused alias. | Emilio Jesus Gallego Arias | |
| No effect on actual code. | |||
| 2018-11-19 | [proof] Provide better control of "open proofs" exceptions. | Emilio Jesus Gallego Arias | |
| This is inspired and an alternative to #8981. We consolidate the "open proof" exception, allowing clients to explicitly capture it and removing some ugly duplicated code in the way. The `Solve Obligation tac` semantics are then tweaked as to removed the wide-scope "catch-all" and indeed will now relay errors in `tac` as it will only absorb tactics that don't error but fail to close the goal such as `auto`. For the rest of the cases, we introduce a warning, and may move to a full error in later releases. We also remove an unnecessary `tclCOMPLETE` call to code that will actually call `close_proof`. In this case, it is better to delegate error management to the core function. Some error messages have changed [as we consolidate two error paths] so this PR may require adjustment in that area. | |||
| 2018-11-18 | [options] Remove deprecated option automatic introduction. | Emilio Jesus Gallego Arias | |
| 2018-11-17 | [vernacextend] Consolidate extension points API | Emilio Jesus Gallego Arias | |
| We group the extension API and datatypes under `Vernacextend`. This means that the base plugin dependency is now `coq.vernac` from `coq.stm`. This is quite important as for example the LSP server won't like to link the STM in. LTAC still depends on the STM by means of the ltac_profile part tho. The next step could be to move the extension point below `Vernacexpr`. | |||
| 2018-11-17 | [pfedit] Remove cook_proof stub. | Emilio Jesus Gallego Arias | |
| This is barely used and not very useful, clients should use the close_proof API directly. | |||
| 2018-11-16 | Use universe names when printing to dot. | Gaëtan Gilbert | |
| 2018-11-16 | Print Universes Subgraph | Gaëtan Gilbert | |
| This adds an optional [Subgraph] part to the Print Universes command, eg [Print Universes Subgraph(i j)] to print only constraints related to i and j (and Prop/Set). | |||
| 2018-11-16 | Print universe names in subtyping error instead of Var(x). | Gaëtan Gilbert | |
| 2018-11-16 | Print full binders in subtyping incompatible polymorphism error. | Gaëtan Gilbert | |
| Close #8891 | |||
| 2018-11-16 | Remove the implicit tactic feature following #7229. | Pierre-Marie Pédrot | |
| 2018-11-14 | Deprecate hint declaration/removal with no specified database | Maxime Dénès | |
| Previously, hints added without a specified database where implicitly put in the "core" database, which was discouraged by the user manual (because of the lack of modularity of this approach). | |||
| 2018-11-13 | Merge PR #8760: Automatically generate names for universes. | Pierre-Marie Pédrot | |
| 2018-11-13 | [vernac] Rename Vernacinterp to Vernacextend and move extension functions there. | Emilio Jesus Gallego Arias | |
| This PR fixes an issues that was bugging me for some time, namely that `Vernacinterp` really means `Vernacextend`. We thus rename the file and move the associated functions there, which were incorrectly placed in `Vernacentries`. Note the beneficial effects on reducing the `.mli` API. | |||
| 2018-11-12 | Don't declare universe binders for variables. | Gaëtan Gilbert | |
| Otherwise ~~~ Unset Strict Universe Declaration. Section bar. Let baz := Type@{u}. Definition k := baz. End bar. Section bar. Let baz := Type@{u}. Definition k' := baz. End bar. ~~~ is broken (and has been since we stopped checking for repeated section names). | |||
| 2018-11-12 | Only declare univ binders once for mutind | Gaëtan Gilbert | |
| 2018-11-12 | Merge PR #8892: Fix part of #8224: grounding open term in fixpoints | Pierre-Marie Pédrot | |
| 2018-11-09 | Merge PR #8601: Move bound universe names to abstract contexts | Gaëtan Gilbert | |
| 2018-11-09 | Use arrays of names instead of lists in abstract universe names. | Pierre-Marie Pédrot | |
| There is little point in having a list, as there is virtually no sharing nor expansion of bound universe names. This representation is thus more compact. | |||
| 2018-11-09 | Remove remnants of polymorphic instance name registration. | Pierre-Marie Pédrot | |
| 2018-11-09 | Force the user to provide names when generating abstract universe contexts. | Pierre-Marie Pédrot | |
| For now this data is not stored, but the code checks that indeed the number of names provided coincide with the instance length. I had to reimplement the same kind of workaround hack in section handling as the one already performed in UnivNames because the name information is not present in the section data structure. This deserves a FIXME. | |||
| 2018-11-09 | Adding universe names to polymorphic entry instances. | Pierre-Marie Pédrot | |
| 2018-11-08 | Standardize handling of Automatic Introduction. | Jasper Hugunin | |
| This fixes #8791. We explicitly specify for intro the names of binders which are given by the user. This still can suffer from spurious collisions, see #8819. | |||
| 2018-11-09 | [topfmt] Add phase attribute for toplevel printing. | Emilio Jesus Gallego Arias | |
| This is localized version of #8833, but instead of adding a phase attribute which, as pointed by @gares has some problematic semantics, we add a local one to the toplevel functions. This moves the imperative part of the API to a better-delimited scope and allows to progress with the separation of the interactive and compilation API. Note that still quite a few issues do remain in the "Feedback" path, for example, idetop and other feedback clients cannot get a hold of the feedback early enough as to direct init messages to the IDE part. This is for example a serious issue of the API that shall be treated separately. | |||
| 2018-11-07 | Merge PR #8773: [checker] Refactor by sharing code with the kernel | Pierre-Marie Pédrot | |
| 2018-11-06 | Move debug term printer to kernel | Maxime Dénès | |
| 2018-11-06 | [program] extend obligation to give back a mapping from obligations to | Matthieu Sozeau | |
| terms This is necessary for programs like Equations that call add_definition and want to later update in their hook some separate datastructures which refer to the obligations that are defined by Program. We give back a map from obligation name to a constr defined in the program's universe state which the hook returns as well. (Obligation names also correspond to undefined evars in the original terms through Obligations.eterm_obligations). Using this, I can avoid ucontext_of_aucontext in Equations, allowing PR #8601 to go through. | |||
| 2018-11-05 | Merge PR #8899: Remove the deprecated Token module and port the ↵ | Emilio Jesus Gallego Arias | |
| corresponding code. | |||
| 2018-11-05 | Merge PR #8871: [library] Move Nametab/Lib specific-names to Nametab | Hugo Herbelin | |
| 2018-11-05 | Merge PR #8515: Command driven attributes | Pierre-Marie Pédrot | |
| 2018-11-05 | Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel ↵ | Maxime Dénès | |
| functions | |||
| 2018-11-04 | Remove the deprecated Token module and port the corresponding code. | Pierre-Marie Pédrot | |
| 2018-11-03 | Merge PR #8852: Use the obligation evar flag | Pierre-Marie Pédrot | |
| 2018-11-02 | Merge PR #8834: [error printing] Fix improper grounding of open terms in ↵ | Hugo Herbelin | |
| printing. | |||
| 2018-11-02 | Universe Polymorphism is a normal attribute modulo the stm (no Flags) | Gaëtan Gilbert | |
| 2018-11-02 | Per command attribute parsing for core commands | Gaëtan Gilbert | |
| 2018-11-02 | Load doesn't support attributes | Gaëtan Gilbert | |
| 2018-11-02 | Simplify use of polymorphism/program globals in attributes | Gaëtan Gilbert | |
| 2018-11-02 | Remove is_universe_polymorphic in indschemes | Gaëtan Gilbert | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |