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

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index a7c0e5b54..f0b2c87f1 100644
--- a/components/tactics/proofEngineHelpers.mli
+++ b/components/tactics/proofEngineHelpers.mli
@@ -103,16 +103,11 @@ 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 ************************************************)
+
+val get_name: Cic.context -> int -> string option
+
+val get_rel: Cic.context -> string -> Cic.term option