added records pp, ast and fixed a bug in match with only one branch

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3c141126d3c26f8c80be266fc8e18588c42016b4..f16b0226678d9ea525c63e5c2bbc6f93e3a36303 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -50,7 +50,7 @@ let tactic_of_ast = function
   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
   | TacticAst.Auto (_,num) -> 
-      AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
+      AutoTactic.auto_tac ~num (MatitaDb.instance ())
   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
 (*
   (* TODO Zack a lot more of tactics to be implemented here ... *)
@@ -63,7 +63,7 @@ let tactic_of_ast = function
   | TacticAst.Replace_pattern of 'term pattern * 'term
 *)
   | TacticAst.LetIn (loc,term,name) ->
-      Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name])
+      Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
   | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
       ProofEngineTypes.mk_tactic 
       (fun (((_,metasenv,_,_),goal) as status) ->
@@ -226,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
@@ -647,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