diff options
| author | Maxime Dénès | 2018-01-12 14:32:43 -0800 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-12 14:32:43 -0800 |
| commit | 13dc988771fe3db8df1cc73900a897549cd10e17 (patch) | |
| tree | a0f7f586c8aa74da49e09dd805d1a43023fc0f24 /checker/values.ml | |
| parent | 3815ec5405976196ff79b6960e65ce5adda66205 (diff) | |
| parent | 72750482070355baf4df6977da75c5448b2b994d (diff) | |
Merge PR #6288: Interfaces for checker and IDE.
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/checker/values.ml b/checker/values.ml index 5a371164c6..4698227ff0 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 |