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 /engine/eConstr.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 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 36297fe243..374cb72753 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -127,9 +127,9 @@ let isRef sigma c = match kind sigma c with let isRefX sigma x c = let open GlobRef in match x, kind sigma c with - | ConstRef c, Const (c', _) -> Constant.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' - | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | ConstRef c, Const (c', _) -> Constant.CanOrd.equal c c' + | IndRef i, Ind (i', _) -> Ind.CanOrd.equal i i' + | ConstructRef i, Construct (i', _) -> Construct.CanOrd.equal i i' | VarRef id, Var id' -> Id.equal id id' | _ -> false @@ -514,7 +514,7 @@ let compare_head_gen_proj env sigma equ eqs eqc' nargs m n = | Proj (p, c), App (f, args) | App (f, args), Proj (p, c) -> (match kind f with - | Const (p', u) when Constant.equal (Projection.constant p) p' -> + | Const (p', u) when Environ.QConstant.equal env (Projection.constant p) p' -> let npars = Projection.npars p in if Array.length args == npars + 1 then eqc' 0 c args.(npars) |