diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1db40e8db..13eb91393 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -180,7 +180,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = raise Elimconst) args in let reversible_rels = List.map fst li in - if not (List.distinct reversible_rels) then + if not (List.distinct_f Int.compare reversible_rels) then raise Elimconst; List.iteri (fun i t_i -> if not (List.mem_assoc (i+1) li) then |