From bb5e6d7c39211349d460db0b61b2caf3d099d5b6 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 23 Oct 2013 22:17:33 +0000 Subject: 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 --- toplevel/lemmas.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'toplevel/lemmas.ml') 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 -- cgit v1.2.3