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/doc/coq-src-description.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev/doc')

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
 
-- 
cgit v1.2.3