X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;fp=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=e477004847961515d090e6250e94d0bd41bd4ae3;hb=5b5dca0c118dfbe3ba8f0514ef07549544eb7810;hp=da50ea2ac17d435c3ffc8c0db6ac0eae9c3253a9;hpb=f00a612006ac05f49a42ab507a95d3298bc1457a;p=helm.git

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index da50ea2ac..e47700484 100644
--- a/matita/components/ng_tactics/nTacStatus.mli
+++ b/matita/components/ng_tactics/nTacStatus.mli
@@ -75,7 +75,7 @@ val disambiguate:
 
 val analyse_indty: 
  #pstatus as 'status -> cic_term -> 
-  'status * (NReference.reference * int * NCic.term list * NCic.term list)
+  'status * (NReference.reference * int * NCic.term list * NCic.term list * NCic.constructor list)
 
 val ppterm: #pstatus -> cic_term -> string
 val ppcontext: #pstatus -> NCic.context -> string
@@ -85,6 +85,8 @@ val whd:
 val normalize: 
  #pstatus as 'status -> ?delta:int -> NCic.context -> cic_term ->
   'status * cic_term 
+val are_convertible: 
+ #pstatus as 'status -> NCic.context -> cic_term -> cic_term -> 'status * bool
 val typeof: 
  #pstatus as 'status -> NCic.context -> cic_term -> 'status * cic_term
 val unify: