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, 6 insertions, 0 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index ab678666fa..734b7853f5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -310,6 +310,12 @@ let destCase c = match kind_of_term c with
 
 let isCase c =  match kind_of_term c with Case _ -> true | _ -> false
 
+let isProj c =  match kind_of_term c with Proj _ -> true | _ -> false
+
+let destProj c = match kind_of_term c with
+  | Proj (p, c) -> (p, c)
+  | _ -> raise DestKO
+
 let destFix c = match kind_of_term c with
   | Fix fix -> fix
   | _ -> raise DestKO