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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 62f4eb1f3..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 []
@@ -239,7 +244,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
@@ -313,21 +318,28 @@ 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))
-  | 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 =
+  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 *)
@@ -337,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)
 
@@ -445,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)
 
@@ -511,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 =