X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=bf39a1caca2170658880b4673bd77b2c7bd7a874;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=503d4a06a9309f925aac65bbd8ab7663a54b2722;hpb=59977ba4636f09f6b2c22c6af9adc5257f2d8a46;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 503d4a06a..bf39a1cac 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 Disambiguate.NoWellTypedInterpretation)
+              | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]]))
         in
         let types = List.fold_left disambiguate [] types in
         GrafiteAst.Decompose (loc, types, what, names)