From f34dcb97406611704c93970ea623d6a8587e5ba8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 12:43:23 +0200
Subject: Moving the remaining Refiner functions to Tacmach.

---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index bca1eb5754..f14edec639 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -186,7 +186,7 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with
 let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
-let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g))
+let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Tacmach.project g))
 let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in
-- 
cgit v1.2.3


From a33f772631696c694f0d9a7fad3a914037c464b2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 26 Jun 2020 12:56:26 +0200
Subject: Refining out the Refiner.

---
 dev/base_include | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index 67ea3a1fa1..1f14fc2941 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -114,7 +114,6 @@ open Logic
 open Proof
 open Proof_using
 open Redexpr
-open Refiner
 open Tacmach
 
 open Hints
-- 
cgit v1.2.3


From 6bb0c6df0dd331b8acb78a720eaf076aea5fce47 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 27 Jun 2020 14:58:17 +0200
Subject: Adding overlay.

---
 dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh b/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh
new file mode 100644
index 0000000000..c8c5b3ed5a
--- /dev/null
+++ b/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12599" ] || [ "$CI_BRANCH" = "rm-deprecated-refiner" ]; then
+
+    equations_CI_REF=rm-deprecated-refiner
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
-- 
cgit v1.2.3