diff options
| author | Pierre-Marie Pédrot | 2018-09-19 08:33:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-19 08:33:35 +0200 |
| commit | 98aedc543d31ca89428e9789fd76529a7409b7cb (patch) | |
| tree | b8bea57e1cf298d7da829ca67d702bc98cccd4b9 /library | |
| parent | 15649c16bc4e20ef2c2b1b0ac645f83ee03c3589 (diff) | |
| parent | 6ab397f8dd3f453d58e2167ca21a9f07aeb2a0c3 (diff) | |
Merge PR #8463: Remove Dischargedhypsmaps
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 |