]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/mathql_generator/cGLocateInductive.ml
Now mathql_generator compiles before mathql_interpreter.
[helm.git] / helm / ocaml / mathql_generator / cGLocateInductive.ml
index 032060fd3d7d4736f1696188c7cd367a2527911e..c5734f2429a173a61c2c7ffd0530339a5a9f1560 100644 (file)
@@ -30,7 +30,7 @@ exception NotAnInductiveDefinition
 
 let get_constraints = function
    | Cic.MutInd (uri, t, _) -> 
-      let uri = MQueryUtil.string_of_uriref (uri, [t]) in
+      let uri = MQueryMisc.string_of_uriref (uri, [t]) in
       let constr_obj =
        [(`InHypothesis, uri); (`MainHypothesis (Some 0), uri)]
       in