X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_tactics%2FnTacStatus.mli;h=e477004847961515d090e6250e94d0bd41bd4ae3;hb=0bcf2dc1a27e38cb6cd3d44eb838d652926841e0;hp=44c95304519fdecdbe787e9081e8957c39e54e21;hpb=dd627e471392375ca7b6dad78a931a8682e06dbe;p=helm.git

diff --git a/matita/components/ng_tactics/nTacStatus.mli b/matita/components/ng_tactics/nTacStatus.mli
index 44c953045..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