Back-portin from new Matita: semantics of ntry changed (fixed?) when applied

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 86b42f66190403dc2630ec8ebe941cb66db75dec..29683eea5c721f412b08e9c7ba584862bcade754 100644 (file)
--- 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 =