From 82ed3089485ebe0b722d8505ddbd89d73570b8f9 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 5 Jul 2016 10:43:48 +0200 Subject: FIX: "dev/doc/changes.txt" --- dev/doc/changes.txt | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'dev') 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 -- cgit v1.2.3