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.

1 files changed, 4 insertions, 0 deletions

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}