X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=29683eea5c721f412b08e9c7ba584862bcade754;hb=e8164f9de889435794efac0fa83fc7b9b766428f;hp=86b42f66190403dc2630ec8ebe941cb66db75dec;hpb=bc044646afa3551066afbc584671a76b86b38855;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 86b42f661..29683eea5 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -261,10 +261,13 @@ let repeat_tac t s =
 
 
 let try_tac tac status =
+ let try_tac status =
   try
     tac status
   with NTacStatus.Error _ ->
     status
+ in
+  atomic_tac try_tac status
 ;;
 
 let first_tac tacl status =
@@ -371,7 +374,7 @@ let select0_tac ~where:(wanted,hyps,where) ~job  =
    let status, instance = 
      mk_meta status newgoalctx (`Decl newgoalty) `IsTerm
    in
-   instantiate status goal instance)
+   instantiate ~refine:false status goal instance)
 ;;
 
 let select_tac ~where ~job move_down_hyps =