diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ecaba603d2..ceb0748fee 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1047,12 +1047,11 @@ let internalise sigma globalenv env allow_patvar lvar c = let idl = Array.map (fun (id,(n,order),bl,ty,bd) -> let intern_ro_arg f = - let idx = Option.default 0 (index_of_annot bl n) in - let before, after = list_chop idx bl in + let before, after = split_at_annot bl n in let ((ids',_,_,_) as env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern (ids', unb, tmp_scope, scopes)) in - let n' = Option.map (fun _ -> List.length before) n in + let n' = Option.map (fun _ -> List.length rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, ((ids',_,_,_),rbl) = |