X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fdeclarative.ml;h=b1b38a9492e76cb5526c24c870382696a5f50314;hb=137a822662f81efbbeac7ddc833fc9ffe252a70e;hp=242d6e3fe6476dab2d100f6253ea72d6d502215a;hpb=8d212b0fb581ab5193be3a3bdfaac8e61cff348c;p=helm.git

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 242d6e3fe..b1b38a949 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -175,7 +175,9 @@ let rewritingstep ~dbd ~universe lhs rhs just conclude =
                 ~continuations:
                   [ Tactics.apply prhs ;
                     Tactics.apply (Cic.Rel 1) ;
-                    just]) status
+                    Tacticals.then_
+                     ~start:(Tactics.clear ~hyps:[last_hyp_name])
+                     ~continuation:just]) status
           | Some name ->
              let mk_fresh_name_callback =
 	      fun metasenv context _ ~typ ->
@@ -193,7 +195,9 @@ let rewritingstep ~dbd ~universe lhs rhs just conclude =
                       ~continuations:
                         [ Tactics.apply prhs ;
                           Tactics.apply (Cic.Rel 1) ;
-                          just]
+                          Tacticals.then_
+                           ~start:(Tactics.clear ~hyps:[last_hyp_name])
+                           ~continuation:just]
                    ]) status)
     | Some lhs ->
        match conclude with
@@ -237,10 +241,12 @@ let case id ~params =
 
 let thesisbecomes t =
 let ty = None in
- (*BUG here: missing check on t *)
  match ty with
-    None -> Tacticals.id_tac
+    None ->
+     Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
+      (fun _ metasenv ugraph -> t,metasenv,ugraph)
   | Some ty ->
+     (*BUG here: missing check on t *)
      Tactics.change ~pattern:(None,[],Some (Cic.Implicit (Some `Hole)))
       (fun _ metasenv ugraph -> ty,metasenv,ugraph)
 ;;