diff options
| author | coqbot-app[bot] | 2020-10-27 12:55:13 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-27 12:55:13 +0000 |
| commit | 5f5cddae48c08872107f30938dcc2f3c8d91f33a (patch) | |
| tree | 2f1bb58c33fee5b4bb0913296ef4341a8832feb4 /pretyping/cases.ml | |
| parent | b87fd6cfe5fe872a38d98c294aea84cde8c6c160 (diff) | |
| parent | 375fc707b402b855770ec32c57ad1362f2a89e5c (diff) | |
Merge PR #13075: Introducing the foundations for a name-alias-agnostic API
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
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 97218ca670..4a29db0dcf 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -515,7 +515,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 @@ -1965,7 +1965,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."); @@ -2193,7 +2193,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 |