X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.mli;h=1eeb0aca3b3356a9168673d20750a35d8d05720e;hb=66929b8edb58d468a134b648466f3e9c45ba5c0e;hp=0b5db790dce1aa66cf9c0c5edc877c355f83eefa;hpb=e31bb143e3a303321e509f415764338849b7e516;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index 0b5db790d..1eeb0aca3 100644
--- a/helm/software/components/tactics/proofEngineHelpers.mli
+++ b/helm/software/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
@@ -103,22 +103,24 @@ val locate_in_conjecture:
  ?equality:(Cic.context -> Cic.term -> Cic.term -> bool) ->
   Cic.term -> Cic.conjecture -> (Cic.context * Cic.term) list
 
-(* saturate_term newmeta metasenv context ty goal_arity                       *)
-(* Given a type [ty] (a backbone), it returns its suffix of length            *)
-(* [goal_arity] head and a new metasenv in which there is new a META for each *)
-(* hypothesis, a list of arguments for the new applications and the index of  *)
-(* the last new META introduced. The nth argument in the list of arguments is *)
-(* just the nth new META.                                                     *)
-val saturate_term:
- int -> Cic.metasenv -> Cic.context -> Cic.term -> int ->
-  Cic.term * Cic.metasenv * Cic.term list * int
-
 (* returns the index and the type of a premise in a context *)
 val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
 
-(* FG: some helper functions ************************************************)
+(* orders a metasenv w.r.t. dependency among metas *)
+val sort_metasenv: Cic.metasenv -> Cic.metasenv
+
 
-val list_rev_map_filter: ('a -> 'b option) -> 'a list -> 'b list
+(* FG: some helper functions ************************************************)
 
 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