Merge branch 'declarative' into matita-lablgtk3

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

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index cfd8c107a49e57784eddd46e6c1ce600cf5e32ca..fea7161c157fbe7a015383d1a2a35252b40434a4 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -26,7 +26,6 @@
 (* $Id$ *)
 
 module G = GrafiteAst
-open GrafiteTypes
 open Printf
 
 class status baseuri =
@@ -51,7 +50,7 @@ let first_line = ref true ;;
 let cases_or_induction_context stack =
     match stack with
      [] -> false
-    | (g,t,k,tag,p)::tl -> try
+    | (_g,_t,_k,_tag,p)::_tl -> try
                             let s = List.assoc "context" p in
                             s = "cases" || s = "induction"
                            with
@@ -61,10 +60,10 @@ let cases_or_induction_context stack =
 let has_focused_goal stack =
     match stack with
      [] -> false
-    | (g,t,k,tag,p)::tl -> (List.length g) > 0
+    | (g,_t,_k,_tag,_p)::_tl -> (List.length g) > 0
 ;;
 
-let get_indentation status statement =
+let get_indentation status _statement =
   let base_ind =
     match status#stack with
       [] -> 0
@@ -105,7 +104,7 @@ let write_ast_to_file status fname statement =
                 | G.NObj (_,obj,_) ->
                         (
                         match obj with
-                            Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
+                            NotationPt.Theorem _ -> "\n" ^ GrafiteAstPp.pp_statement status statement
                                    ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
                         |   _ -> ""
                         )
@@ -252,17 +251,17 @@ let baseuri_of_script ~include_paths fname =
 
 (* given a path to a ma file inside the include_paths, returns the
    new include_paths associated to that file *)
-let read_include_paths ~include_paths file =
-  try
-    let root, _buri, _fname, _tgt =
-      Librarian.baseuri_of_script ~include_paths:[] file in
-    let includes =
-      try
-        Str.split (Str.regexp " ")
-          (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
-      with Not_found -> []
-    in
-    let rc = root :: includes in
+let read_include_paths ~include_paths:_ file =
+ try 
+   let root, _buri, _fname, _tgt = 
+     Librarian.baseuri_of_script ~include_paths:[] file in 
+   let includes =
+    try
+     Str.split (Str.regexp " ") 
+      (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+    with Not_found -> []
+   in
+   let rc = root :: includes in
     List.iter (HLog.debug) rc; rc
   with Librarian.NoRootFor _ | Librarian.FileNotFound _ ->
     []