X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=da50ea2ac17d435c3ffc8c0db6ac0eae9c3253a9;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=35e74debf70b315efee950816a8f4a65276c809b;hpb=225887a9f23aac79d4cca907da026917b7df04dc;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