- ng_refiner:

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

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index 35e74debf70b315efee950816a8f4a65276c809b..da50ea2ac17d435c3ffc8c0db6ac0eae9c3253a9 100644 (file)
--- 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