aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-07-05 10:43:48 +0200
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-07-05 10:43:48 +0200
commit82ed3089485ebe0b722d8505ddbd89d73570b8f9 (patch)
tree662e9121ee2e28fe62e938cb766479bc6205df2b /dev
parentb2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385 (diff)
FIX: "dev/doc/changes.txt"
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.txt8
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