X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineHelpers.mli;h=1eeb0aca3b3356a9168673d20750a35d8d05720e;hb=63adafe5fb700c8ecf13f74fc31086c173617e86;hp=1ac3ee707f17c7ef3eca3f7ec284885c9d5107a8;hpb=acc9067d3263ffced81c52539f918d47d418d5c7;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineHelpers.mli b/helm/software/components/tactics/proofEngineHelpers.mli
index 1ac3ee707..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
@@ -106,6 +106,10 @@ 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