aboutsummaryrefslogtreecommitdiff
path: root/interp/stdarg.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-03-10 10:04:56 +0100
committerMaxime Dénès2018-03-10 10:04:56 +0100
commit4d5c7243b4aea5b28358757e2d86c11334da6699 (patch)
treeade1ab73a9c2066302145bb3781a39b5d46b4513 /interp/stdarg.ml
parent93a1c4786c9b17efdda025f754ad97376d61a9ba (diff)
parentb1d749e59444f86e40f897c41739168bb1b1b9b3 (diff)
Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.
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 0958cc7eee..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 {CAst.loc;v=(s,_)} -> loc
-
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"