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 /pretyping/cases.ml | |
| 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 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index a459229256..d48951e84a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -514,7 +514,7 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with let loc = pat.CAst.loc in (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in - if eq_ind ind' ind then + if Ind.CanOrd.equal ind' ind then (* Check the constructor has the right number of args *) let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in @@ -1936,7 +1936,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let realnal = match t with | Some {CAst.loc;v=(ind',realnal)} -> - if not (eq_ind ind ind') then + if not (Ind.CanOrd.equal ind ind') then user_err ?loc (str "Wrong inductive type."); if not (Int.equal nrealargs_ctxt (List.length realnal)) then anomaly (Pp.str "Ill-formed 'in' clause in cases."); @@ -2164,7 +2164,7 @@ let constr_of_pat env sigma arsign pat avoid = in let (ind,u), params = dest_ind_family indf in let params = List.map EConstr.of_constr params in - if not (eq_ind ind cind) then error_bad_constructor ?loc env cstr ind; + if not (Ind.CanOrd.equal ind cind) then error_bad_constructor ?loc env cstr ind; let cstrs = get_constructors env indf in let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in |