From 4f81cc44e5af01f40ad972a7285edd2c40c178c7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 7 Mar 2020 01:04:46 -0500
Subject: [proof] Start of mutual definition save refactoring.

First commit of a series that will unify (and enforce) the handling of
mutual constants. We will split this in several commits as to easy
debugging / bisect in case of problems.

In this first commit, we move the actual declare logic to a common
place.
---
 tactics/proof_global.ml  | 8 --------
 tactics/proof_global.mli | 4 +---
 2 files changed, 1 insertion(+), 11 deletions(-)

(limited to 'tactics')

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 7fd1634dcf..623e6b8a42 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -8,14 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(***********************************************************************)
-(*                                                                     *)
-(*      This module defines proof facilities relevant to the           *)
-(*      toplevel. In particular it defines the global proof            *)
-(*      environment.                                                   *)
-(*                                                                     *)
-(***********************************************************************)
-
 open Util
 open Names
 open Context
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index f1281d1291..e1c75c0649 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -8,9 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** This module defines proof facilities relevant to the
-     toplevel. In particular it defines the global proof
-     environment. *)
+(** State for interactive proofs. *)
 
 type t
 
-- 
cgit v1.2.3