diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 | ||||
| -rw-r--r-- | vernac/recLemmas.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 475d4e9af9..f715459616 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -496,7 +496,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let u,v = try destruct_ind env sigma tt1 (* trick so that the good sequence is returned*) with e when CErrors.noncritical e -> indu,[||] - in if eq_ind (fst u) ind + in if Ind.CanOrd.equal (fst u) ind then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ] else ( find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 5f7eb78a40..bef9e29ac2 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -656,7 +656,7 @@ let explain_evar_not_found env sigma id = let explain_wrong_case_info env (ind,u) ci = let pi = pr_inductive env ind in - if eq_ind ci.ci_ind ind then + if Ind.CanOrd.equal ci.ci_ind ind then str "Pattern-matching expression on an object of inductive type" ++ spc () ++ pi ++ spc () ++ str "has invalid information." else @@ -1232,7 +1232,7 @@ let error_not_allowed_dependent_analysis env isrec i = pr_inductive env i ++ str "." let error_not_mutual_in_scheme env ind ind' = - if eq_ind ind ind' then + if Ind.CanOrd.equal ind ind' then str "The inductive type " ++ pr_inductive env ind ++ str " occurs twice." else diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml index 79468627de..af72c01758 100644 --- a/vernac/recLemmas.ml +++ b/vernac/recLemmas.ml @@ -70,7 +70,7 @@ let find_mutually_recursive_statements sigma thms = | [], _::_ -> let () = match same_indccl with | ind :: _ -> - if List.distinct_f Names.ind_ord (List.map pi1 ind) + if List.distinct_f Names.Ind.CanOrd.compare (List.map pi1 ind) then Flags.if_verbose Feedback.msg_info (Pp.strbrk |