aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/csymtable.ml')
-rw-r--r--kernel/csymtable.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 2bbb867cd..bbd284bc1 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 =