From d833b81b49366e95cf20a1d00f9c63883adb8942 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 03:04:13 +0100
Subject: Rewrite API using EConstr.

---
 engine/termops.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index 7c89f190f2..ecc6ab68ea 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -858,6 +858,11 @@ let base_sort_cmp pb s0 s1 =
     | (Type u1, Type u2) -> true
     | _ -> false
 
+let rec is_Prop sigma c = match EConstr.kind sigma c with
+  | Sort (Prop Null) -> true
+  | Cast (c,_,_) -> is_Prop sigma c
+  | _ -> false
+
 (* eq_constr extended with universe erasure *)
 let compare_constr_univ sigma f cv_pb t1 t2 =
   match EConstr.kind sigma t1, EConstr.kind sigma t2 with
-- 
cgit v1.2.3