- ProofEngineHelpers: namer_of moved to GrafiteEngine

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

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index f0b2c87f12fc14a2b8f8ac3d477c7654a023cc9f..39fb69b0d1067370a408c62be07cc495331516c1 100644 (file)
--- 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
@@ -106,8 +106,25 @@ val locate_in_conjecture:
 (* returns the index and the type of a premise in a context *)
 val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
 
+(* orders a metasenv w.r.t. dependency among metas *)
+val sort_metasenv: Cic.metasenv -> Cic.metasenv
+
+
 (* 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
+   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