X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMisc.ml;h=41b96793884d88546a2cd42ce06101551ddeef44;hb=532cedb4dfaee23bbddffa70801f6abf604bd436;hp=58fa388091e7c165ff76783141c82e6d55efd798;hpb=de9a83f286eee12117fb478ea2db18f7faebac9a;p=helm.git

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 58fa38809..41b967938 100644
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -169,6 +169,8 @@ let get_proof_context status =
       let (_, context, _) = CicUtil.lookup_meta goal metasenv in
       context
   | _ -> []
+ 
+let get_proof_aliases status = status.aliases
   
 let qualify status name = get_string_option status "baseuri" ^ "/" ^ name