diff options
| author | Maxime Dénès | 2018-09-11 18:35:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-18 08:36:41 +0200 |
| commit | 6ab397f8dd3f453d58e2167ca21a9f07aeb2a0c3 (patch) | |
| tree | aa9e00f6c21d0f86e6252b2bf5e69b77f1ed06ca /library | |
| parent | f1482433ff225831d9937753f946cff2577b9309 (diff) | |
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.
Diffstat (limited to 'library')
| -rw-r--r-- | library/dischargedhypsmap.ml | 21 | ||||
| -rw-r--r-- | library/dischargedhypsmap.mli | 19 | ||||
| -rw-r--r-- | library/library.mllib | 1 |
3 files changed, 0 insertions, 41 deletions
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 |