diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2e5ec38c8b..74ea5aef6a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -789,8 +789,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let lf = List.map (fun (id,_,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = - try - (list_index iddef lf) -1 + try list_index0 iddef lf with Not_found -> raise (InternalisationError (locid,UnboundFixName (false,iddef))) in @@ -827,8 +826,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let lf = List.map (fun (id,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = - try - (list_index iddef lf) -1 + try list_index0 iddef lf with Not_found -> raise (InternalisationError (locid,UnboundFixName (true,iddef))) in |