diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-07-05 10:43:48 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-07-05 10:43:48 +0200 |
| commit | 82ed3089485ebe0b722d8505ddbd89d73570b8f9 (patch) | |
| tree | 662e9121ee2e28fe62e938cb766479bc6205df2b /dev | |
| parent | b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385 (diff) | |
FIX: "dev/doc/changes.txt"
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 3cd371bfd..feef80ed3 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -190,8 +190,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id Now it is represented as: - Context.Rel.t = LocalAssum of Names.Name.t * Constr.t - | LocalDef of Names.Name.t * Constr.t * Constr.t + Context.Rel.Declaration.t = LocalAssum of Names.Name.t * Constr.t + | LocalDef of Names.Name.t * Constr.t * Constr.t - Originally, named-context was represented as: @@ -199,8 +199,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id Now it is represented as: - Context.Named.t = LocalAssum of Names.Id.t * Constr.t - | LocalDef of Names.Id.t * Constr.t * Constr.t + Context.Named.Declaration.t = LocalAssum of Names.Id.t * Constr.t + | LocalDef of Names.Id.t * Constr.t * Constr.t - The various EXTEND macros do not handle specially the Coq-defined entries anymore. Instead, they just output a name that have to exist in the scope |