aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2019-05-21 13:53:06 +0200
committerHugo Herbelin2019-05-21 20:48:04 +0200
commitd14be61b4468573d7aa184fe6c8a0a7c8d5a0044 (patch)
treeba06defe9bd29c40a2beffb8f9bbf2851836b5fa
parent897088fb8f4769bacca9fc289387096283835cd6 (diff)
Fixing an indentation in constrintern.ml.
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f06493b374..7fbf808a11 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1845,7 +1845,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
in
apply_impargs c env imp subscopes l loc
- | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
+ | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =