diff options
| author | Maxime Dénès | 2018-02-14 14:20:17 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-14 14:20:17 +0100 |
| commit | ce7a851f21bd6e7c811bd3b7520019dabe609afc (patch) | |
| tree | bdabb07656b1c218c581a575e97cbb703b246b23 /kernel/csymtable.ml | |
| parent | 4f65dfb13d8bb395abf4aa405cae9ed529302a06 (diff) | |
| parent | 07e861c1792fcc3bde091640ee5e42b398cfa6da (diff) | |
Merge PR #6713: Fix #6677: Critical bug with VM and universes
Diffstat (limited to 'kernel/csymtable.ml')
| -rw-r--r-- | kernel/csymtable.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 2bbb867cd4..bbd284bc1d 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -70,7 +70,7 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn _, _ -> false | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false -| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type u1, Const_type u2 -> Univ.Universe.equal u1 u2 | Const_type _ , _ -> false let rec hash_structured_constant c = |