DisambiguationError exceptions (that have locations inside) are now relocated

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 503d4a06a9309f925aac65bbd8ab7663a54b2722..84291dcc6582866cdfa31c06d5683cbb4130788d 100644 (file)
--- 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 Disambiguate.NoWellTypedInterpretation)
+              | _ -> 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)
@@ -676,11 +676,11 @@ let eval_from_moo_ref = ref (fun _ _ _ -> assert false);;
 let disambiguate_obj status obj =
   let uri =
    match obj with
-      GrafiteAst.Inductive (_,(name,_,_,_)::_)
-    | GrafiteAst.Record (_,name,_,_) ->
+    | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+    | CicNotationPt.Record (_,name,_,_) ->
        Some (UriManager.uri_of_string (MatitaTypes.qualify status name ^ ".ind"))
-    | GrafiteAst.Inductive _ -> assert false
-    | GrafiteAst.Theorem _ -> None in
+    | CicNotationPt.Inductive _ -> assert false
+    | CicNotationPt.Theorem _ -> None in
   let (diff, metasenv, cic, _) =
     singleton
       (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
@@ -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
@@ -850,7 +849,7 @@ let eval_command opts status cmd =
          if opts.do_heavy_checks then
            begin
              let dbd = MatitaDb.instance () in
-             let similar = MetadataQuery.match_term ~dbd ty in
+             let similar = Whelp.match_term ~dbd ty in
              let similar_len = List.length similar in
              if similar_len> 30 then
                (MatitaLog.message