X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=8aae7633a9222fd8f8dc86b0a3d737369827492b;hb=bb49c457d64878ed9611656f620548b5151e5dbd;hp=ae933d2d0022a1f08d7dca832f633a8024840ebe;hpb=15a4844b5d8f64a72964e5a917b6bd6d8d7dbe44;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index ae933d2d0..8aae7633a 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -25,7 +25,8 @@ let tactic_of_ast = function
       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Intros (_, Some num, names) ->
       (* TODO Zack implement intros length *)
-      PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
+      PrimitiveTactics.intros_tac ~howmany:num
+        ~mk_fresh_name_callback:(namer_of names) ()
   | TacticAst.Reflexivity _ -> Tactics.reflexivity
   | TacticAst.Assumption _ -> Tactics.assumption
   | TacticAst.Contradiction _ -> Tactics.contradiction
@@ -225,8 +226,15 @@ let eval_coercion status coercion =
     aux ty
   in
   let ty_src,ty_tgt = extract_last_two_p coer_ty in
-  let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in
-  let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in
+  let context = [] in 
+  let src_uri = 
+    let ty_src = CicReduction.whd context ty_src in
+    UriManager.uri_of_string (CicUtil.uri_of_term ty_src) 
+  in
+  let tgt_uri = 
+    let ty_tgt = CicReduction.whd context ty_tgt in
+    UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) 
+  in
   let new_coercions =
     (* also adds them to the Db *)
     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
@@ -335,7 +343,6 @@ let eval_command status cmd =
         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") 
       in
       let metasenv = MatitaMisc.get_proof_metasenv status in
-      debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body);
       let (body_type, ugraph) =
         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
       in
@@ -343,8 +350,9 @@ let eval_command status cmd =
         CicUnification.fo_unif metasenv [] body_type ty ugraph
       in
       if metasenv <> [] then
-        command_error
-          "metasenv not empty while giving a definition with body";
+        command_error (
+          "metasenv not empty while giving a definition with body: " ^
+          CicMetaSubst.ppmetasenv metasenv []) ;
       let body = CicMetaSubst.apply_subst subst body in
       let ty = CicMetaSubst.apply_subst subst ty in
       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
@@ -646,9 +654,8 @@ let disambiguate_executable status ex =
       let status, cmd = disambiguate_command status cmd in
       status, (TacticAst.Command (loc, cmd))
   | TacticAst.Macro (_, mac) -> 
-      command_error 
-        (sprintf ("The engine is not allowed to disambiguate any macro, "^^
-                 "in particular %s") (TacticAstPp.pp_macro_ast mac))
+      command_error (sprintf "The macro %s can't be in a script" 
+        (TacticAstPp.pp_macro_ast mac))
 
 let disambiguate_comment status c = 
   match c with