X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=9279de399ab954e671faf1ee23eb59f682323508;hb=9730627f1ab5a6071f7e3f615e23bf6696f7041e;hp=f32511265b3cd4c5c624e5317646fed2a1da31e4;hpb=e603c19e82c160362587cb0bc578287c87122b90;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index f32511265..9279de399 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -11,8 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-exception Error of string lazy_t
-val fail: string lazy_t -> 'a
+exception Error of string lazy_t * exn option
+val fail: ?exn:exn -> string lazy_t -> 'a
 
 class pstatus :
  NCic.obj ->
@@ -55,6 +55,7 @@ val refine:
   'status * cic_term * cic_term (* status, term, type *)
 val apply_subst:
  #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
+val fix_sorts: cic_term -> cic_term
 
 val get_goalty: #pstatus -> int -> cic_term
 val mk_meta: 
@@ -74,7 +75,7 @@ val mk_in_scope: #pstatus as 'status -> cic_term -> 'status * cic_term
 val mk_out_scope:
  int -> (#pstatus as 'status) -> cic_term -> 'status * cic_term
 
-val pp_tac_status: #pstatus -> unit
+val pp_status: #pstatus -> unit
 
 class ['stack] status :
  NCic.obj -> 'stack ->