X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineHelpers.mli;h=1ac3ee707f17c7ef3eca3f7ec284885c9d5107a8;hb=2d0ff020fc7100546d4f87560062721cd401ccae;hp=f0b2c87f12fc14a2b8f8ac3d477c7654a023cc9f;hpb=6bb370c6e1a036e82315765d6dceb1939c30ed23;p=helm.git

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index f0b2c87f1..1ac3ee707 100644
--- a/components/tactics/proofEngineHelpers.mli
+++ b/components/tactics/proofEngineHelpers.mli
@@ -111,3 +111,12 @@ val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
 val get_name: Cic.context -> int -> string option
 
 val get_rel: Cic.context -> string -> Cic.term option
+
+(* split_with_whd (c, t) takes a type t typed in the context c and returns
+   [(c_0, t_0); (c_1, t_1); ...; (c_n, t_n)], n where t_0 is the conclusion of
+   t and t_i is the premise of t accessed by Rel i in t_0. 
+   Performes a whd on the conclusion before giving up.
+   Each t_i is returned with a context c_i in wich it is typed
+*)
+val split_with_whd: Cic.context * Cic.term -> 
+                    (Cic.context * Cic.term) list * int