From 2bbf1305a080667d8547c44b2684010aba3d8d45 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Tue, 30 Sep 2014 01:18:24 +0200
Subject: Simplify evarconv thanks to new delta status of projections, using
 whd_state_gen to handle unfolding. Add an isProj/destProj in term. Use the
 proper environment everywhere in unification.ml.

---
 kernel/term.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 28ebc41e2..50cd433e9 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -112,6 +112,7 @@ val isConstruct : constr -> bool
 val isFix : constr -> bool
 val isCoFix : constr -> bool
 val isCase : constr -> bool
+val isProj : constr -> bool
 
 val is_Prop : constr -> bool
 val is_Set  : constr -> bool
@@ -183,6 +184,9 @@ return P in t1], or [if c then t1 else t2])
 where [info] is pretty-printing information *)
 val destCase : constr -> case_info * constr * constr * constr array
 
+(** Destructs a projection *)
+val destProj : constr -> projection * constr
+
 (** Destructs the {% $ %}i{% $ %}th function of the block
    [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
     with    f{_ 2} ctx{_ 2} = b{_ 2}
-- 
cgit v1.2.3