Add support for proving cases in a different order

[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 44c95304519fdecdbe787e9081e8957c39e54e21..e477004847961515d090e6250e94d0bd41bd4ae3 100644 (file)
--- 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