X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=da50ea2ac17d435c3ffc8c0db6ac0eae9c3253a9;hb=48c011f52853dd106dbf9cbbd1b9da61277fba3b;hp=35e74debf70b315efee950816a8f4a65276c809b;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index 35e74debf..da50ea2ac 100644
--- a/matita/components/ng_tactics/nTacStatus.mli
+++ b/matita/components/ng_tactics/nTacStatus.mli
@@ -70,7 +70,7 @@ val term_of_cic_term :
 
 val mk_cic_term : NCic.context -> NCic.term -> cic_term
 val disambiguate:
- #pstatus as 'status -> NCic.context -> tactic_term -> cic_term option ->
+ #pstatus as 'status -> NCic.context -> tactic_term -> cic_term NCicRefiner.expected_type ->
   'status * cic_term (* * cic_term XXX *)
 
 val analyse_indty: 
@@ -90,7 +90,7 @@ val typeof:
 val unify: 
  #pstatus as 'status -> NCic.context -> cic_term -> cic_term -> 'status
 val refine: 
- #pstatus as 'status -> NCic.context -> cic_term -> cic_term option -> 
+ #pstatus as 'status -> NCic.context -> cic_term -> cic_term NCicRefiner.expected_type -> 
   'status * cic_term * cic_term (* status, term, type *)
 val apply_subst:
  #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term