aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ef92ff3bc2..74740abcef 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -335,7 +335,7 @@ let check_capture loc ty = function
()
let locate_if_isevar loc na = function
- | RHole _ -> RHole (loc, AbstractionType na))
+ | RHole _ -> RHole (loc, AbstractionType na)
| x -> x
(**********************************************************************)