X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fmathql_generator%2FcGMatchConclusion.ml;h=70dfde4755b1aa8ffed2ef4175943d6e2426d8d0;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4f739763a6b9b96b58f2332c7eba71600eafdb12;hpb=3ac183ee3dd4eea25d61bd4c5be4f7db9f829a7e;p=helm.git

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index 4f739763a..70dfde475 100644
--- 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) =
@@ -41,7 +43,6 @@ let sort_entries entries =
 let levels_of_term metasenv context term =
    let module TC = CicTypeChecker in
    let module Red = CicReduction in
-   let module Util = MQueryUtil in
    let degree t =
       let rec degree_aux = function
          | Cic.Sort _         -> 1 
@@ -49,7 +50,7 @@ let levels_of_term metasenv context term =
          | Cic.Prod (_, _, t) -> degree_aux t
          | _                  -> 2
       in 
-      let u = TC.type_of_aux' metasenv context t in
+      let u,_ = TC.type_of_aux' metasenv context t CicUniv.empty_ugraph in
       degree_aux (Red.whd context u)
    in
    let entry_eq (s1, b1, v1) (s2, b2, v2) =
@@ -62,16 +63,19 @@ let levels_of_term metasenv context term =
    in
    let inspect_uri main l uri tc v term =
       let d = degree term in 
-      entry_in (Util.string_of_uriref (uri, tc), main, 2 * v + d - 1) l 
+      entry_in (UriManager.string_of_uriref (uri, tc), main, 2 * v + d - 1) l 
    in
    let rec inspect_term main l v term = match term with
         Cic.Rel _                        -> l
       | Cic.Meta _                       -> l
       | Cic.Sort _                       -> l 
-      | Cic.Implicit                     -> l 
+      | Cic.Implicit _                   -> l 
       | Cic.Var (u,exp_named_subst)      ->
-         let l' = inspect_uri main l u [] v term in
+         inspect_exp_named_subst l (succ v) exp_named_subst
+(*
+	 let l' = inspect_uri main l u [] v term in
           inspect_exp_named_subst l' (succ v) exp_named_subst
+*)      
       | Cic.Const (u,exp_named_subst)    ->
          let l' = inspect_uri main l u [] v term in
           inspect_exp_named_subst l' (succ v) exp_named_subst
@@ -151,3 +155,5 @@ let get_constraints e c t =
 	 mk_musts (prev @ [acc]) acc next
    in
    mk_musts [] [] can   
+
+let universe = [T.MainConclusion; T.InConclusion]