diff options
Diffstat (limited to 'vernac/lemmas.ml')
-rw-r--r-- | vernac/lemmas.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index dbf7fec66..22f0d199c 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -116,7 +116,7 @@ let find_mutually_recursive_statements thms = [] in ind_hyps,ind_ccl) thms in let inds_hyps,ind_ccls = List.split inds in - let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> eq_mind kn kn' in + let of_same_mutind ((kn,_),_,_) = function ((kn',_),_,_) -> MutInd.equal kn kn' in (* Check if all conclusions are coinductive in the same type *) (* (degenerated cartesian product since there is at most one coind ccl) *) let same_indccl = |