From a9f8fa56e76aa557b1391cb9709cb893a4f602ce Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 23 Aug 2017 12:37:36 +0200 Subject: Using EConstr equality check in unification. The code from Universes what essentially a duplicate of the one from EConstr, but they were copied for historical reasons. Now, this is not useful anymore, so that we remove the implementation from Universes and rely on the one from EConstr. --- engine/eConstr.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'engine/eConstr.ml') diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 7b879a803..66b50fc25 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -566,7 +566,6 @@ let compare_constr sigma cmp c1 c2 = let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2) -(** TODO: factorize with universes.ml *) let test_constr_universes sigma leq m n = let open Universes in let kind c = kind_upto sigma c in -- cgit v1.2.3