Yet another implementation of the single aliases / multi aliases idea.

[helm.git] / helm / matita / matitaMisc.mli

diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli
index 568bcc5ed8ee9270825957d1b95a80660fb98f64..21045c0a3b1134e5429c50ab2296fcedf979dd96 100644 (file)
--- a/helm/matita/matitaMisc.mli
+++ b/helm/matita/matitaMisc.mli
@@ -113,7 +113,6 @@ val get_proof_status: MatitaTypes.status -> ProofEngineTypes.status
 val get_proof_metasenv: MatitaTypes.status ->  Cic.metasenv
 val get_proof_context: MatitaTypes.status -> Cic.context 
 val get_proof_conclusion: MatitaTypes.status -> Cic.term 
-val get_proof_aliases: MatitaTypes.status -> DisambiguateTypes.environment 
 
   (** given the base name of an image, returns its full path *)
 val image_path: string -> string