From 417641e48129c9ba8656c622c9b64cd32641e7de Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Nov 2018 20:16:41 +0100
Subject: [legacy proof engine] Remove some cruft.

We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.

This is not a lot but every little step helps.
---
 dev/base_include                                               | 1 -
 dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh | 6 ++++++
 dev/doc/coq-src-description.txt                                | 2 +-
 dev/top_printers.mli                                           | 4 ++--
 4 files changed, 9 insertions(+), 4 deletions(-)
 create mode 100644 dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index 0e12b57b36..d2e8f6d092 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -135,7 +135,6 @@ open Pfedit
 open Proof
 open Proof_using
 open Proof_global
-open Proof_type
 open Redexpr
 open Refiner
 open Tacmach
diff --git a/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
new file mode 100644
index 0000000000..c8bea0c868
--- /dev/null
+++ b/dev/ci/user-overlays/08998-ejgallego-legacy_proof_eng_clean.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8998" ] || [ "$CI_BRANCH" = "legacy_proof_eng_clean" ]; then
+
+    equations_CI_REF=legacy_proof_eng_clean
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index 764d482957..e5e4f740bd 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -94,7 +94,7 @@ Tacexpr.glob_tactic_expr
  |
  | Tacinterp.eval_tactic (?)
  V
-Proof_type.tactic
+Proofview.V82.tac
 
 TODO: check with Hugo
 
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index eaa12ff702..5eac3e2b9c 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -120,9 +120,9 @@ val ppclenv : Clenv.clausenv -> unit
 
 val ppgoalgoal : Goal.goal -> unit
 
-val ppgoal : Proof_type.goal Evd.sigma -> unit
+val ppgoal : Goal.goal Evd.sigma -> unit
 (* also print evar map *)
-val ppgoalsigma : Proof_type.goal Evd.sigma -> unit
+val ppgoalsigma : Goal.goal Evd.sigma -> unit
 
 val pphintdb : Hints.Hint_db.t -> unit
 val ppproofview : Proofview.proofview -> unit
-- 
cgit v1.2.3