diff options
author | 2016-12-27 16:53:30 +0100 | |
---|---|---|
committer | 2016-12-27 18:33:25 +0100 | |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /kernel/sorts.ml | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'kernel/sorts.ml')
-rw-r--r-- | kernel/sorts.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/sorts.ml b/kernel/sorts.ml index a9073688..62013b38 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -98,7 +98,7 @@ module Hsorts = let u' = huniv u in if u' == u then c else Type u' | s -> s - let equal s1 s2 = match (s1,s2) with + let eq s1 s2 = match (s1,s2) with | (Prop c1, Prop c2) -> c1 == c2 | (Type u1, Type u2) -> u1 == u2 |_ -> false |