- generalize finished

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

diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index df862f223f436a26b35bf90cc6e569ed71a94ba0..3963f2500943ad1c6a793b8202398025b6e0af87 100644 (file)
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -33,7 +33,8 @@ type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input
 
 type cic_term 
 val ctx_of : cic_term -> NCic.context
-val term_of_cic_term : cic_term -> NCic.context -> NCic.term
+val term_of_cic_term : 
+      lowtac_status -> cic_term -> NCic.context -> lowtac_status * NCic.term
 
 val mk_cic_term : NCic.context -> NCic.term -> cic_term
 type ast_term = string * int * CicNotationPt.term
@@ -43,10 +44,14 @@ val disambiguate:
 
 val analyse_indty: 
   lowtac_status -> cic_term -> 
-    NReference.reference * int * NCic.term list * NCic.term list
-
-val whd: lowtac_status -> ?delta:int -> NCic.context -> cic_term -> cic_term 
-val typeof: lowtac_status -> NCic.context -> cic_term -> cic_term
+    lowtac_status * 
+      (NReference.reference * int * NCic.term list * NCic.term list)
+
+val whd: 
+      lowtac_status -> ?delta:int -> NCic.context -> cic_term -> 
+        lowtac_status * cic_term 
+val typeof: 
+      lowtac_status -> NCic.context -> cic_term -> lowtac_status * cic_term
 val unify: 
   lowtac_status -> NCic.context -> cic_term -> cic_term -> lowtac_status
 val refine: