X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=ec9f7738aac7314fad72944c0d43a7cf145aacf7;hb=a22628e5de37d3ffe9de056d7683f2ebdf7226fb;hp=f3bdd5aa146436723058a05a808c9e3a06542575;hpb=1e16d80cc7bf9b73cf5526934b17e2ba955a522a;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index f3bdd5aa1..ec9f7738a 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -56,7 +56,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 fix_sorts: #pstatus as 'status -> cic_term -> 'status * cic_term
 val saturate :
  #pstatus as 'status -> ?delta:int -> cic_term -> 'status * cic_term * cic_term list
 val metas_of_term : #pstatus as 'status -> cic_term -> int list
@@ -64,7 +64,7 @@ val metas_of_term : #pstatus as 'status -> cic_term -> int list
 val get_goalty: #pstatus -> int -> cic_term
 val mk_meta: 
  #pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
-   [ `Decl of cic_term | `Def of cic_term ] ->
+   [ `Decl of cic_term | `Def of cic_term ] -> NCicUntrusted.meta_kind ->
      'status * cic_term
 val instantiate: #pstatus as 'status -> int -> cic_term -> 'status
 val instantiate_with_ast: #pstatus as 'status -> int -> tactic_term -> 'status