diff options
| -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 |