aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/values.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-30 13:01:48 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-10 18:27:28 +0100
commit8c59f1a464a446191f48358fe2484ec65ac0ef1c (patch)
tree85701335471ba6a62bc267d01747fc26c5e5c665 /checker/values.ml
parentd439c01190f45de5ac493b8f55d361503e83ad03 (diff)
Add interfaces for checker and remove dead code.
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml19
1 files changed, 0 insertions, 19 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 5a371164c..4698227ff 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -372,22 +372,3 @@ let v_lib =
let v_opaques = Array (v_computation v_constr)
let v_univopaques =
Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
-
-(** Registering dynamic values *)
-
-module IntOrd =
-struct
- type t = int
- let compare (x : t) (y : t) = compare x y
-end
-
-module IntMap = Map.Make(IntOrd)
-
-let dyn_table : value IntMap.t ref = ref IntMap.empty
-
-let register_dyn name t =
- dyn_table := IntMap.add name t !dyn_table
-
-let find_dyn name =
- try IntMap.find name !dyn_table
- with Not_found -> Any