...

[helm.git] / helm / software / components / ng_tactics / nTacStatus.mli

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 3fdc0330d9b1d6800c572c739564d9acdb728eaa..33b01b5753e08d350b3f3a5dbeea4a1c3536882e 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -55,10 +55,11 @@ 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: 
- #pstatus as 'status -> ?name:string -> NCic.context ->
+ #pstatus as 'status -> ?attrs:NCic.meta_attrs -> NCic.context ->
    [ `Decl of cic_term | `Def of cic_term ] ->
      'status * cic_term
 val instantiate: #pstatus as 'status -> int -> cic_term -> 'status