- tacticals: new tactical ifs added: uses thens where if_ uses then_

[helm.git] / components / tactics / proofEngineHelpers.mli

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index 1eeb0aca3b3356a9168673d20750a35d8d05720e..cc13d1ad780bf067e7df4ca65ee77ef4bd447ca2 100644 (file)
--- a/components/tactics/proofEngineHelpers.mli
+++ b/components/tactics/proofEngineHelpers.mli
@@ -121,6 +121,15 @@ val get_rel: Cic.context -> string -> Cic.term option
    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
+   split_with_normalize (c, t) normalizes t before operating the split
+   whd is useless here
 *)
 val split_with_whd: Cic.context * Cic.term -> 
                     (Cic.context * Cic.term) list * int
+val split_with_normalize: Cic.context * Cic.term -> 
+                          (Cic.context * Cic.term) list * int
+
+(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
+  * names as long as they are available, then it fallbacks to name generation
+  * using FreshNamesGenerator module *)
+val namer_of: string option list -> ProofEngineTypes.mk_fresh_name_type