aboutsummaryrefslogtreecommitdiff
path: root/interp/stdarg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/stdarg.ml')
-rw-r--r--interp/stdarg.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 5f1aad0c25..e5ed58be6b 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Misctypes
open Genarg
open Geninterp
@@ -32,10 +31,6 @@ let wit_string : string uniform_genarg_type =
let wit_pre_ident : string uniform_genarg_type =
make0 "preident"
-let loc_of_or_by_notation f = function
- | AN c -> f c
- | ByNotation (loc,(s,_)) -> loc
-
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"