X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FnewConstraints.mli;fp=helm%2Focaml%2Ftactics%2FnewConstraints.mli;h=d81c66fb03080f4d95c329cc0414e92099710cb2;hp=e57d6b1e0a03532d2b09522a929b9b145f7802b7;hb=6150b8ef905aaea17b47ff466c067054f976cd8f;hpb=bd59745a232bff0e941e97170b88709d0ff6fdf2

diff --git a/helm/ocaml/tactics/newConstraints.mli b/helm/ocaml/tactics/newConstraints.mli
index e57d6b1e0..d81c66fb0 100644
--- a/helm/ocaml/tactics/newConstraints.mli
+++ b/helm/ocaml/tactics/newConstraints.mli
@@ -40,15 +40,21 @@ module SetSet : Set.S with type elt = StringSet.t
 
 val pp_SetSet : SetSet.t -> string
 
+val pp_StringSet : StringSet.t -> string
+
+
+
 val inspect_term : int -> Cic.term -> string option * SetSet.t
 
 val prefixes : int -> Cic.term -> string option * ((int * (StringSet.elt list)) list) 
 
-(* (constants_of t) returns a pair (b,n) where n is the number of 
+(* (constants_of t) returns a pair (b,n) where n is the set of the
    constants in the conclusion of t, and b is true if in MainConclusion
    we have an equality *)
 
 val constants_of : Cic.term -> bool * StringSet.t
 
+val constants_concl : Cic.term -> StringSet.t
+
 val pp_prefixes : ((int * (StringSet.elt list)) list) -> string