X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=84291dcc6582866cdfa31c06d5683cbb4130788d;hb=8653d506aacaf019deb3438bd4681ad1000061bd;hp=b62dd23deabd9ecd24375cb0ced9153fed7c6510;hpb=c1f74c5fe5c69d3d830f6a58bc0e20c99d1fa8f7;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b62dd23de..84291dcc6 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -253,7 +253,7 @@ let disambiguate_tactic status goal tactic =
               with
               | Cic.MutInd (uri, tyno, _) ->
                   (GrafiteAst.Type (uri, tyno) :: types)
-              | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]]))
+              | _ -> raise (MatitaDisambiguator.DisambiguationError (0,[[None,lazy "Decompose works only on inductive types"]])))
         in
         let types = List.fold_left disambiguate [] types in
         GrafiteAst.Decompose (loc, types, what, names)
@@ -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