diff options
| author | Pierre-Marie Pédrot | 2020-09-23 13:58:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:23:19 +0200 |
| commit | aa3d78fefde6897a50273c83f944b6617963a9bc (patch) | |
| tree | c24d9916af4b51762d4bde46f3ac5ea78d9c09d6 /pretyping | |
| parent | bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc (diff) | |
Similar introduction of a Construct module in the Names API.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 2 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 0200b32ef2..d394bd1288 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -246,7 +246,7 @@ let matches_core env sigma allow_bound_rels | VarRef id, Var id' -> Names.Id.equal id id' | ConstRef c, Const (c',_) -> Environ.QConstant.equal env c c' | IndRef i, Ind (i', _) -> Names.Ind.CanOrd.equal i i' - | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' + | ConstructRef c, Construct (c',u) -> Names.Construct.CanOrd.equal c c' | _, _ -> false in let rec sorec ctx env subst p t = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index baab41fa26..1940668519 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -589,7 +589,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty end | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') - when Names.eq_constructor cons cons' -> + when Names.Construct.CanOrd.equal cons cons' -> if EInstance.is_empty u && EInstance.is_empty u' then Success evd else let u = EInstance.kind evd u and u' = EInstance.kind evd u' in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 43032790e2..bdf3495479 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -91,7 +91,7 @@ let case_style_eq s1 s2 = let open Constr in match s1, s2 with let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with | PatVar na1, PatVar na2 -> Name.equal na1 na2 | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) -> - eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 && + Construct.CanOrd.equal c1 c2 && List.equal cases_pattern_eq pl1 pl2 && Name.equal na1 na2 | (PatVar _ | PatCstr _), _ -> false |