diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-11 20:29:16 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-28 14:16:52 +0200 |
| commit | 0ade32f84b28d2190360ec79520788142755b5b7 (patch) | |
| tree | 46b2d11c817707c3b84653b490de3b0aaad42038 /checker/term.ml | |
| parent | bd8606189268c3fcdd3506872d459cb9032a33bf (diff) | |
[api] Deprecate a couple of aliases that we missed.
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/term.ml b/checker/term.ml index 19034a57d..0236f7867 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -390,7 +390,7 @@ let compare_constr f t1 t2 = f h1 h2 && List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2 - | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2 + | Const c1, Const c2 -> eq_puniverses Constant.UserOrd.equal c1 c2 | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2 | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2 && Univ.Instance.equal u1 u2 |