]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql_test/mqgtop.ml
CGLocateInductive patched
[helm.git] / helm / mathql_test / mqgtop.ml
index aba3bb3d4e85846ec70f31f2ca1725713cb48627..edf714b1e6a1ecb0e6f2216079182d68d84a6617 100644 (file)
@@ -232,7 +232,7 @@ let mbackward n m l =
 
 let inductive l = 
    let queries = ref [] in
-   let univ = Some C3.universe in 
+   let univ = None in 
    let handle = get_handle () in
    let rec aux = function
       | []           -> ()