attached macros: hint(partial), check

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

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index 58fa388091e7c165ff76783141c82e6d55efd798..41b96793884d88546a2cd42ce06101551ddeef44 100644 (file)
--- 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