diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-23 12:37:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-08 20:46:08 +0200 |
| commit | a9f8fa56e76aa557b1391cb9709cb893a4f602ce (patch) | |
| tree | 9ef357486083ebefa0a9b2ef328270b74f5dad93 /engine/eConstr.ml | |
| parent | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (diff) | |
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.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 |