- added and exposed get_current_status_as_xml

[helm.git] / helm / gTopLevel / mQueryLevels2.ml

diff --git a/helm/gTopLevel/mQueryLevels2.ml b/helm/gTopLevel/mQueryLevels2.ml
index afd0ee42b957c4bb6311003c35e2185cdb5fc09c..968d2a35e8d6439c65c0549bc35d7f58c372f383 100644 (file)
--- a/helm/gTopLevel/mQueryLevels2.ml
+++ b/helm/gTopLevel/mQueryLevels2.ml
@@ -169,14 +169,13 @@ in
  let obj_constraints,rel_constraints,sort_constraints =
   process_type_aux (Backbone 0) (CicMiniReduction.letin_nf term)
  in
-  (obj_constraints,rel_constraints,sort_constraints),
-   (Some obj_constraints,Some rel_constraints,Some sort_constraints)
+  (obj_constraints,rel_constraints,sort_constraints)
 ;;
 
 (*CSC: Debugging only *)
 let get_constraints term =
  let res = get_constraints term in
- let ((objs,rels,sorts),can) = res in
+ let (objs,rels,sorts) = res in
   prerr_endline "Constraints on objs:" ;
   List.iter
    (function (s1,s2,n) ->
@@ -197,6 +196,5 @@ let get_constraints term =
       (s1 ^ " " ^ (match n with Some n' -> string_of_int n' | None -> "NULL") ^
         " " ^ s2)
    ) sorts ;
-  prerr_endline "The \"only\" constraints are the same." ;
   res
 ;;