From 27190db7f119bc9b50150be6dff889986c747e38 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 21 Nov 2016 15:05:26 -0500
Subject: (v8.6) Add example in dev/doc/changes involving Tacmach.project

---
 dev/doc/changes.txt | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index d052468f99..e926674696 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -244,6 +244,10 @@ define_evar_* mostly used internally in the unification engine.
   ...
   let Sigma (xn, sigma, pn) = ... in
   Sigma (ans, sigma, p1 +> ... +> pn)
+  
+  Examples of `Sigma.Unsafe.of_evar_map` include:
+  
+  Evarutil.new_evar env (Tacmach.project goal) ty   ----> Evarutil.new_evar env (Sigma.Unsafe.of_evar_map (Tacmach.project goal)) ty
 
 - The Proofview.Goal.*enter family of functions now takes a polymorphic
   continuation given as a record as an argument.
-- 
cgit v1.2.3


From 8572140c30629cfcc6b7e68d450487c64922a6b9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 21 Nov 2016 16:01:34 -0500
Subject: (v8.6) Make a note about wit_constr and Constrarg in dev/doc/changes

---
 dev/doc/changes.txt | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index d052468f99..12c0163b95 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -218,6 +218,8 @@ val get_id_for_feedback : unit -> edit_or_state_id * route_id
   for constructing compound entries still works over this scheme. Note that in
   the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
   in the parsing rules, so beware of recursive calls.
+  
+  For example, to get "wit_constr" you must "open Constrarg" at the top of the file.
 
 - Evarutil was split in two parts. The new Evardefine file exposes functions
 define_evar_* mostly used internally in the unification engine.
-- 
cgit v1.2.3


From 59dee24e5dfe3dfe20c2a4a2843192d797c89155 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 21 Nov 2016 17:03:22 -0500
Subject: (v8.6) Update dev/doc/changes with things about mem_named_context

---
 dev/doc/changes.txt | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index d052468f99..156f38c455 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -256,7 +256,10 @@ define_evar_* mostly used internally in the unification engine.
 
   Proofview.Goal.enter { enter = begin fun gl -> ... end }
   
-- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c`
+- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` ---> `Tacinterp.Value.of_constr c`
+- `Pretyping.Termops.mem_named_context`                      ---> `Engine.Termops.mem_named_context_val`
+  (`Global.named_context`                                    ---> `Global.named_context_val`)
+  (`Context.Named.lookup`                                    ---> `Environ.lookup_named_val`)
 
 ** Search API **
 
-- 
cgit v1.2.3


From bfa2ac5fc5578d9bcf2ea1183deeaa6329c29b9b Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 21 Nov 2016 17:11:45 -0500
Subject: (v8.6) Update dev/doc/changes.txt with HintsResolveEntry changes

---
 dev/doc/changes.txt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index d052468f99..134a6a25e8 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -256,7 +256,8 @@ define_evar_* mostly used internally in the unification engine.
 
   Proofview.Goal.enter { enter = begin fun gl -> ... end }
   
-- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c`
+- `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)`      ---> `Tacinterp.Value.of_constr c`
+- `Vernacexpr.HintsResolveEntry(priority, poly, hnf, path, atom)` ---> `Vernacexpr.HintsResolveEntry(Vernacexpr.({hint_priority = priority; hint_pattern = None}), poly, hnf, path, atom)`
 
 ** Search API **
 
-- 
cgit v1.2.3