X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FprimitiveTactics.ml;h=ca6b0e58234d59737de1c71660887231e51ee9d6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f38dd10b3108c13a991d6ad00b73b0868bbb0ca3;hpb=04ade947888ac1115dfe104714bed61c32e1c9c3;p=helm.git

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index f38dd10b3..ca6b0e582 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -67,7 +67,7 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
          in
           context, t, (C.Meta (newmeta,irl))
         else
-         raise (Fail "intro(s): not enough products or let-ins")
+         raise (Fail (lazy "intro(s): not enough products or let-ins"))
   in
    collect_context context howmany ty 
 
@@ -152,7 +152,12 @@ let classify_metas newmeta in_subst_domain subst_in metasenv =
             | Some (n,Cic.Def (s,None)) ->
                Some (n,Cic.Def ((subst_in canonical_context' s),None))
             | None -> None
-            | Some (_,Cic.Def (_,Some _)) -> assert false
+            | Some (n,Cic.Def (bo,Some ty)) ->
+               Some
+                (n,
+                  Cic.Def
+                   (subst_in canonical_context' bo,
+                    Some (subst_in canonical_context' ty)))
           in
            entry'::canonical_context'
         ) canonical_context []
@@ -325,10 +330,9 @@ let apply_tac_verbose_with_subst ~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))
-  | CicTypeChecker.TypeCheckerFailure _ as e ->
-      raise (Fail (Printexc.to_string e))
+  | CicUnification.UnificationFailure msg
+  | CicTypeChecker.TypeCheckerFailure msg ->
+      raise (Fail msg)
 
 (* ALB *)
 let apply_tac_verbose ~term status =
@@ -345,10 +349,9 @@ let apply_tac ~term =
     apply_tac ~term status
       (* TODO cacciare anche altre eccezioni? *)
   with 
-  | CicUnification.UnificationFailure _ as e ->
-      raise (Fail (Printexc.to_string e))
-  | CicTypeChecker.TypeCheckerFailure _ as e ->
-      raise (Fail (Printexc.to_string e))
+  | CicUnification.UnificationFailure msg
+  | CicTypeChecker.TypeCheckerFailure msg ->
+      raise (Fail msg)
  in
   mk_tactic (apply_tac ~term)
 
@@ -453,7 +456,7 @@ let exact_tac ~term =
     (newproof, [])
    end
   else
-   raise (Fail "The type of the provided term is not the one expected.")
+   raise (Fail (lazy "The type of the provided term is not the one expected."))
  in
   mk_tactic (exact_tac ~term)
 
@@ -519,10 +522,8 @@ let elim_tac ~term =
           in
            C.Appl (eliminator_ref :: make_tl term (args_no - 1))
          in
-          let metasenv', term_to_refine' =
-           CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in
           let refined_term,_,metasenv'',_ = 
-           CicRefine.type_of_aux' metasenv' context term_to_refine' 
+           CicRefine.type_of_aux' metasenv' context term_to_refine
              CicUniv.empty_ugraph
           in
            let new_goals =