diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:33 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:33 +0000 |
| commit | bb5e6d7c39211349d460db0b61b2caf3d099d5b6 (patch) | |
| tree | e14b120edc5fedcb1a0a114218d1cdaa0f887ed4 /toplevel/lemmas.ml | |
| parent | 4e20ed9e5c1608226f0d736df10bb82fc402e7a2 (diff) | |
cList: a few alternative to hashtbl-based uniquize, distinct, subset
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/lemmas.ml')
| -rw-r--r-- | toplevel/lemmas.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index a25f96d46..519112dfd 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -135,8 +135,13 @@ let find_mutually_recursive_statements thms = | [], _::_ -> let () = match same_indccl with | ind :: _ -> - if List.distinct (List.map pi1 ind) then - if_verbose msg_info (strbrk "Coinductive statements do not follow the order of definition, assuming the proof to be by induction."); flush_all () + if List.distinct_f ind_ord (List.map pi1 ind) + then + if_verbose msg_info + (strbrk + ("Coinductive statements do not follow the order of "^ + "definition, assuming the proof to be by induction.")); + flush_all () | _ -> () in let possible_guards = List.map (List.map pi3) inds_hyps in |