diff options
| author | Arnaud Spiwack | 2015-02-19 16:35:42 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-02-24 16:37:04 +0100 |
| commit | 2f41d8e976621b907925546a192e90e60f0e580b (patch) | |
| tree | c6cad6b836d9d92cffac90058f98e500559e72da /library | |
| parent | 50edb9bb8d43b190996d1d85a2bfd95f52b2db19 (diff) | |
Refactoring in [Constr].
[compare_head_gen] defined in terms of [compare_head_gen_leq]. Remove an unused argument from [compare_head_gen_leq].
Diffstat (limited to 'library')
| -rw-r--r-- | library/universes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/universes.ml b/library/universes.ml index 79070763ec..51c2b4d851 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -165,7 +165,7 @@ let leq_constr_univs_infer univs m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts + Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in @@ -213,7 +213,7 @@ let leq_constr_universes m n = m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n in let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n + Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n and leq_constr' m n = m == n || compare_leq m n in let res = compare_leq m n in res, !cstrs |