diff options
| author | Pierre-Marie Pédrot | 2020-09-23 12:42:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:22:12 +0200 |
| commit | bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc (patch) | |
| tree | 6cf8e0f459ff3630ebd5115773c04bc0bcd70b6c /vernac | |
| parent | 0a46af10ffc38726207bca952775102d48ad3b15 (diff) | |
Introduce an Ind module in the Names API.
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
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 |