More informative exceptions raised.

[helm.git] / helm / ocaml / tactics / primitiveTactics.ml

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 97f40205201446fdf82cebd6ad5a67278edec6c7..74a9f63f2548290bb22e136e58cf9ae2f9ee06f2 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -239,7 +239,7 @@ let rec count_prods context ty =
     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
   | _ -> 0
 
-let apply_tac_verbose ~term (proof, goal) =
+let apply_tac_verbose_with_subst ~term (proof, goal) =
   (* Assumption: The term "term" must be closed in the current context *)
  let module T = CicTypeChecker in
  let module R = CicReduction in
@@ -281,7 +281,8 @@ let apply_tac_verbose ~term (proof, goal) =
    in
    let metasenv' = metasenv@newmetasenvfragment in
    let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph in
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+   in
    let termty =
      CicSubstitution.subst_vars exp_named_subst_diff termty in
    let goal_arity = count_prods context ty in
@@ -304,7 +305,6 @@ let apply_tac_verbose ~term (proof, goal) =
    in
    let bo' = apply_subst t in
    let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
-(*    prerr_endline ("me: " ^ CicMetaSubst.ppmetasenv newmetasenv'' subst); *)
    let subst_in =
      (* if we just apply the subtitution, the type is irrelevant:
               we may use Implicit, since it will be dropped *)
@@ -313,22 +313,30 @@ let apply_tac_verbose ~term (proof, goal) =
    let (newproof, newmetasenv''') = 
      subst_meta_and_metasenv_in_proof proof metano subst_in newmetasenv''
    in
-     (subst_in,
-       (newproof, 
-          List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+   (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
+    (newproof, 
+     List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
 
-let apply_tac ~term status = snd (apply_tac_verbose ~term status)
 
-let apply_tac_verbose ~term status =
+(* ALB *)
+let apply_tac_verbose_with_subst ~term status =
   try
-    apply_tac_verbose ~term status
+(*     apply_tac_verbose ~term status *)
+    apply_tac_verbose_with_subst ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
-  | CicUnification.UnificationFailure _ as e -> 
-      raise (Fail (Printexc.to_string e))
+  | CicUnification.UnificationFailure msg -> 
+      raise (Fail (CicUnification.explain_error msg))
   | CicTypeChecker.TypeCheckerFailure _ as e ->
       raise (Fail (Printexc.to_string e))
 
+(* ALB *)
+let apply_tac_verbose ~term status =
+  let subst, status = apply_tac_verbose_with_subst ~term status in
+  (CicMetaSubst.apply_subst subst), status
+
+let apply_tac ~term status = snd (apply_tac_verbose ~term status)
+
   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
   sollevino _solamente_ Fail *)
 let apply_tac ~term =
@@ -337,8 +345,8 @@ let apply_tac ~term =
     apply_tac ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
-  | CicUnification.UnificationFailure _ as e ->
-      raise (Fail (Printexc.to_string e))
+  | CicUnification.UnificationFailure msg ->
+      raise (Fail (CicUnification.explain_error msg))
   | CicTypeChecker.TypeCheckerFailure _ as e ->
       raise (Fail (Printexc.to_string e))
  in