From 93a77f3cb8ee36072f93b4c0ace6f0f9c19f51a3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 18:41:37 +0100
Subject: Moving Refine to its proper module.

---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 7710033dba..c46f6b72a4 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -184,6 +184,7 @@ Proof_errors
 Logic_monad
 Proofview_monad
 Proofview
+Refine
 Proof
 Proof_global
 Pfedit
-- 
cgit v1.2.3


From 08c31f46aa05098e1a97d9144599c1e5072b7fc3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 19:52:54 +0100
Subject: Pushing Proofview further down the dependency alley.

---
 dev/printers.mllib | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index c46f6b72a4..db86bb5edd 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -141,6 +141,9 @@ Find_subterm
 Tacred
 Classops
 Typeclasses_errors
+Logic_monad
+Proofview_monad
+Proofview
 Typeclasses
 Detyping
 Indrec
@@ -181,9 +184,6 @@ Refiner
 Clenv
 Evar_refiner
 Proof_errors
-Logic_monad
-Proofview_monad
-Proofview
 Refine
 Proof
 Proof_global
-- 
cgit v1.2.3


From e98d7276f52c4b67bf05a80a6b44f334966f82fd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 20:11:50 +0100
Subject: Splitting Evarutil in two distinct files.

Some parts of Evarutils were related to the management of evars under constraints.
We put them in the Evardefine file.
---
 dev/printers.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index db86bb5edd..4830b36ab5 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -131,6 +131,7 @@ Retyping
 Cbv
 Pretype_errors
 Evarutil
+Evardefine
 Evarsolve
 Recordops
 Evarconv
-- 
cgit v1.2.3


From c3de822e711fa3f10817432b7023fc2f88c0aeeb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 20:41:17 +0100
Subject: Making Evarutil independent from Reductionops.

---
 dev/printers.mllib | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 4830b36ab5..a3ba42ba78 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -123,14 +123,15 @@ Evd
 Sigma
 Glob_ops
 Redops
+Pretype_errors
+Evarutil
 Reductionops
 Inductiveops
 Arguments_renaming
 Nativenorm
 Retyping
 Cbv
-Pretype_errors
-Evarutil
+
 Evardefine
 Evarsolve
 Recordops
-- 
cgit v1.2.3


From 6d87fd89abdf17ddd4864386d66bb06f0d0a151f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Mar 2016 21:20:29 +0100
Subject: Documenting changes.

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

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 1f5ba7862f..2f631c6338 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -76,6 +76,11 @@
   the case of (VERNAC) ARGUMENT EXTEND, the name of the argument entry is bound
   in the parsing rules, so beware of recursive calls.
 
+- Evarutil was split in two parts. The new Evardefine file exposes functions
+define_evar_* mostly used internally in the unification engine.
+
+- The Refine module was move out of Proofview.
+
 =========================================
 = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 =
 =========================================
-- 
cgit v1.2.3