X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2FproofEngineHelpers.mli;h=39fb69b0d1067370a408c62be07cc495331516c1;hb=refs%2Ftags%2F0.4.95%407852;hp=0a053ece7dcd212f1e37aef499ee6e6977529705;hpb=a1c4c601850c71e094a4703af00f02ca2026d8ed;p=helm.git

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index 0a053ece7..39fb69b0d 100644
--- a/components/tactics/proofEngineHelpers.mli
+++ b/components/tactics/proofEngineHelpers.mli
@@ -35,7 +35,7 @@ val subst_meta_in_proof :
   ProofEngineTypes.proof * Cic.metasenv
 val subst_meta_and_metasenv_in_proof :
   ProofEngineTypes.proof ->
-  int -> (Cic.term -> Cic.term) -> Cic.metasenv ->
+  int -> Cic.substitution -> Cic.metasenv ->
   ProofEngineTypes.proof * Cic.metasenv
 
 (* returns the list of goals that are in newmetasenv and were not in
@@ -121,6 +121,10 @@ 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