From 6ab397f8dd3f453d58e2167ca21a9f07aeb2a0c3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 11 Sep 2018 18:35:21 +0200
Subject: Removing Dischargedhypsmap which is unused internally.

The Dischargedhypsmap table collected the segment of section variables
that constants defined in a section were originally depending on. It
was useful to reconstruct the structure of sections as originally
given in a source file. In particular this was used in Sacerdoti
Coen's plugin for exportation of Coq files to xml. There is no
information that this plugin, moved out of Coq in September 2014, was
finally maintained, even as an external plugin. So it seems that the
Dischargedhypsmap table is virtually not used anymore in the wild.

Please contact the developers if ever the need for such a table
happens to be necessary for your work.
---
 library/dischargedhypsmap.ml  | 21 ---------------------
 library/dischargedhypsmap.mli | 19 -------------------
 library/library.mllib         |  1 -
 3 files changed, 41 deletions(-)
 delete mode 100644 library/dischargedhypsmap.ml
 delete mode 100644 library/dischargedhypsmap.mli

(limited to 'library')

diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
deleted file mode 100644
index abcdb93a27..0000000000
--- a/library/dischargedhypsmap.ml
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Libnames
-
-type discharged_hyps = full_path list
-
-let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis"
-
-let set_discharged_hyps sp hyps =
-  discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map
-
-let get_discharged_hyps sp =
-  try Spmap.find sp !discharged_hyps_map with Not_found -> []
diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli
deleted file mode 100644
index c70677225b..0000000000
--- a/library/dischargedhypsmap.mli
+++ /dev/null
@@ -1,19 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Libnames
-
-type discharged_hyps = full_path list
-
-(** Discharged hypothesis. Here we store the discharged hypothesis of each
-    constant or inductive type declaration. *)
-
-val set_discharged_hyps : full_path -> discharged_hyps -> unit
-val get_discharged_hyps : full_path -> discharged_hyps
diff --git a/library/library.mllib b/library/library.mllib
index 9cacaba4a7..8f694f4a31 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -11,7 +11,6 @@ Loadpath
 Library
 States
 Kindops
-Dischargedhypsmap
 Goptions
 Decls
 Keys
-- 
cgit v1.2.3