diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-10-11 19:41:23 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-06-26 13:52:52 +0200 |
commit | af0a04b8e16c2554e0c747da6d625799b332f5fe (patch) | |
tree | dc73cbe7d56a1eea7bb7c22ab1576d0ffa673b11 /kernel/constr.ml | |
parent | a1fc621b943dbf904705dc88ed27c26daf4c5e72 (diff) |
Remove Sorts.contents
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r-- | kernel/constr.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index e68f906ec..45812b5a1 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -130,8 +130,8 @@ let mkProp = Sort Sorts.prop let mkSet = Sort Sorts.set let mkType u = Sort (Sorts.Type u) let mkSort = function - | Sorts.Prop Sorts.Null -> mkProp (* Easy sharing *) - | Sorts.Prop Sorts.Pos -> mkSet + | Sorts.Prop -> mkProp (* Easy sharing *) + | Sorts.Set -> mkSet | s -> Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) @@ -260,17 +260,17 @@ let isSort c = match kind c with | _ -> false let rec isprop c = match kind c with - | Sort (Sorts.Prop _) -> true + | Sort (Sorts.Prop | Sorts.Set) -> true | Cast (c,_,_) -> isprop c | _ -> false let rec is_Prop c = match kind c with - | Sort (Sorts.Prop Sorts.Null) -> true + | Sort Sorts.Prop -> true | Cast (c,_,_) -> is_Prop c | _ -> false let rec is_Set c = match kind c with - | Sort (Sorts.Prop Sorts.Pos) -> true + | Sort Sorts.Set -> true | Cast (c,_,_) -> is_Set c | _ -> false |