aboutsummaryrefslogtreecommitdiff
path: root/interp/impargs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/impargs.ml')
-rw-r--r--interp/impargs.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/interp/impargs.ml b/interp/impargs.ml
index d83a0ce918..90fb5a2036 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -120,8 +120,6 @@ let argument_position_eq p1 p2 = match p1, p2 with
| Hyp h1, Hyp h2 -> Int.equal h1 h2
| _ -> false
-let explicitation_eq = Constrexpr_ops.explicitation_eq
-
type implicit_explanation =
| DepRigid of argument_position
| DepFlex of argument_position