Reshaped structure of ocaml/ libraries, matita changed accordingly.

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index 4413f9b8a3bbc0726c752a1cdd53fcafe564df71..3fa4e93e7bf71ed7c68a74f306fc7f74f4daba4e 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -237,7 +237,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
       let term = disambiguate_macro_term term status user_goal in
-      let l =  MQ.match_term ~dbd term in
+      let l =  Whelp.match_term ~dbd term in
       let query_url =
         MatitaMisc.strip_suffix ~suffix:"."
           (HExtlib.trim_blanks unparsed_text)
@@ -247,12 +247,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
       [], parsed_text_length
   | TA.WInstance (loc, term) ->
       let term = disambiguate_macro_term term status user_goal in
-      let l = MQ.instance ~dbd term in
+      let l = Whelp.instance ~dbd term in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WLocate (loc, s) -> 
-      let l = MQ.locate ~dbd s in
+      let l = Whelp.locate ~dbd s in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
@@ -263,7 +263,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
         | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None 
         | _ -> failwith "Not a MutInd"
       in
-      let l = MQ.elim ~dbd uri in
+      let l = Whelp.elim ~dbd uri in
       let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length