added support for dump/restore/clear proof checker cache

[helm.git] / helm / ocaml / mathql_generator / cGMatchConclusion.ml

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index 4f739763a6b9b96b58f2332c7eba71600eafdb12..28639c8f72a444044a633d5cd7ebfa9b347d159a 100644 (file)
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -26,6 +26,8 @@
 (*  AUTOR: Ferruccio Guidi <fguidi@cs.unibo.it>
  *)
 
+module T = MQGTypes
+
 let text_of_entries out entries =
    out "(** MatchConclusion: results of the term inspection **)\n";
    let text_of_entry (u, b, v) =
@@ -151,3 +153,5 @@ let get_constraints e c t =
         mk_musts (prev @ [acc]) acc next
    in
    mk_musts [] [] can   
+
+let universe = [T.MainConclusion; T.InConclusion]