]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaEngine.ml
removed dead code (thanks to ocaml 3.09)
[helm.git] / helm / matita / matitaEngine.ml
index 72b252140b3a9400383f718fdd3dccfb2dabeefa..10d29cac200c122153348ae0aa2d9fbb94f6f6e7 100644 (file)
@@ -732,7 +732,7 @@ let make_absolute paths path =
    in
    try
      aux paths
-   with Unix.Unix_error _ as exc -> raise (UnableToInclude path)
+   with Unix.Unix_error _ -> raise (UnableToInclude path)
 ;;
        
 let eval_command opts status cmd =
@@ -789,7 +789,6 @@ let eval_command opts status cmd =
                "name/uri. This should be fixed!")
         | _-> command_error "You can't Qed an incomplete theorem"
       in
-      let suri = UriManager.string_of_uri uri in
       if metasenv <> [] then 
         command_error "Proof not completed! metasenv is not empty!";
       let name = UriManager.name_of_uri uri in