auto rewritten with only one tail recursive function.

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

diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli
index 1ac3ee707f17c7ef3eca3f7ec284885c9d5107a8..0a053ece7dcd212f1e37aef499ee6e6977529705 100644 (file)
--- a/components/tactics/proofEngineHelpers.mli
+++ b/components/tactics/proofEngineHelpers.mli
@@ -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