debian version 0.0.6-6

[helm.git] / helm / ocaml / tactics / newConstraints.mli

diff --git a/helm/ocaml/tactics/newConstraints.mli b/helm/ocaml/tactics/newConstraints.mli
index e57d6b1e0a03532d2b09522a929b9b145f7802b7..52c2d7169668ccd52a0422c71910a30c30e1eb85 100644 (file)
--- a/helm/ocaml/tactics/newConstraints.mli
+++ b/helm/ocaml/tactics/newConstraints.mli
@@ -40,15 +40,22 @@ 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
 
+val mainandcons : Cic.term -> (string *  StringSet.t)