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/constr_matching.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/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 71ef166ff0..0200b32ef2 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -245,7 +245,7 @@ let matches_core env sigma allow_bound_rels match ref, EConstr.kind sigma c with | VarRef id, Var id' -> Names.Id.equal id id' | ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c' - | IndRef i, Ind (i', _) -> Names.eq_ind i i' + | IndRef i, Ind (i', _) -> Names.Ind.CanOrd.equal i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' | _, _ -> false in @@ -374,7 +374,7 @@ let matches_core env sigma allow_bound_rels | Some ind1 -> (* ppedrot: Something spooky going here. The comparison used to be the generic one, so I may have broken something. *) - if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure + if not (Ind.CanOrd.equal ind1 ci2.ci_ind) then raise PatternMatchingFailure in let () = if not ci1.cip_extensible && not (Int.equal (List.length br1) n2) |