renamed Http_client to Http_user_agent to avoid clashes with Gerd's

[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 28639c8f72a444044a633d5cd7ebfa9b347d159a..1e721a456bf1d99795ea367d96032e04807ba431 100644 (file)
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -43,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 
@@ -64,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