X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=bf39a1caca2170658880b4673bd77b2c7bd7a874;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1d3b1f94e0d74c58525610eca3894e4e9bb46363;hpb=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 1d3b1f94e..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)
@@ -614,8 +614,11 @@ let eval_coercion status coercion =
   let new_coercions =
     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
   let status =
-   List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
+   List.fold_left (fun s (uri,o,_) -> 
+      let status = MatitaSync.add_obj uri o status in
+      {status with coercions = uri :: status.coercions})
     status new_coercions in
+  let status = {status with coercions = coer_uri :: status.coercions} in
   let statement_of name =
     GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, 
       (CicNotationPt.Ident (name, None)))
@@ -1015,6 +1018,7 @@ let initial_status =
     proof_status = No_proof;
     options = default_options ();
     objects = [];
+    coercions = [];
     notation_ids = [];
   }