diff options
| author | Pierre-Marie Pédrot | 2016-11-20 03:04:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:31 +0100 |
| commit | d833b81b49366e95cf20a1d00f9c63883adb8942 (patch) | |
| tree | 1afca49fcd42e96b658c90d28e9da692ccc39724 /engine/termops.ml | |
| parent | c0d38ae52ac410811e7df54c52e8d3a18bb11bcb (diff) | |
Rewrite API using EConstr.
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 5 |
1 files changed, 5 insertions, 0 deletions
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 |