diff options
Diffstat (limited to 'plugins/omega/coq_omega.ml')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index adf926958..a2016cb03 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1714,7 +1714,7 @@ let onClearedName2 id tac = end }) let rec is_Prop sigma c = match EConstr.kind sigma c with - | Sort (Prop Null) -> true + | Sort s -> Sorts.is_prop (ESorts.kind sigma s) | Cast (c,_,_) -> is_Prop sigma c | _ -> false |