diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 908010428f..2e2389f091 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -555,7 +555,7 @@ let free_rels m = let collect_metas c = let rec collrec acc c = match kind_of_term c with - | Meta mv -> List.add_set mv acc + | Meta mv -> List.add_set Int.equal mv acc | _ -> fold_constr collrec acc c in List.rev (collrec [] c) |