diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 74a49152ca..2c44d6da37 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1334,7 +1334,7 @@ let internalize 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.index0 iddef lf + try List.index0 Id.equal iddef lf with Not_found -> raise (InternalizationError (locid,UnboundFixName (false,iddef))) in @@ -1375,7 +1375,7 @@ let internalize 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.index0 iddef lf + try List.index0 Id.equal iddef lf with Not_found -> raise (InternalizationError (locid,UnboundFixName (true,iddef))) in |