X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=596a74e2e5fa1a837c7335a8faf3233462dedd6d;hb=72aa8b2087285826b14fc39a389632f0317c51b6;hp=dab608e8ad0311e37c2c45456a257e8434cbabb0;hpb=421056da7b3e1d6b9d91d72092b4f3c3232a00ce;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index dab608e8a..596a74e2e 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -157,6 +157,7 @@ let block_tac l status =
   List.fold_left (fun status tac -> tac status) status l
 ;;
 
+
 let compare_statuses ~past ~present =
  let _,_,past,_,_ = past#obj in 
  let _,_,present,_,_ = present#obj in 
@@ -179,17 +180,16 @@ let compare_statuses ~past ~present =
    (e.g. the tactic could perform a global analysis of the set of goals)
 *)
 
-let exec tac low_status g =
+let exec tac (low_status : #lowtac_status) g =
   let stack = [ [0,Open g], [], [], `NoTag ] in
   let status =
-   (new NTacStatus.status low_status#obj stack)#set_estatus
-    (low_status :> NEstatus.status)
+   (new NTacStatus.status low_status#obj stack)#set_estatus low_status
   in
   let status = tac status in
-   (low_status#set_estatus (status :> NEstatus.status))#set_obj status#obj
+   (low_status#set_estatus status)#set_obj status#obj
 ;;
 
-let distribute_tac tac status =
+let distribute_tac tac (status : #tac_status) =
   match status#stack with
   | [] -> assert false
   | (g, t, k, tag) :: s ->
@@ -226,10 +226,19 @@ let distribute_tac tac status =
       let stack =
         (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
       in
-       ((status#set_stack stack)#set_obj (sn :> lowtac_status)#obj)#set_estatus (sn :> NEstatus.status)
+       ((status#set_stack stack)#set_obj(sn:>lowtac_status)#obj)#set_estatus sn
+;;
+
+let atomic_tac htac : #tac_status as 'a -> 'a = distribute_tac (exec htac) ;;
+
+let repeat_tac t s = 
+  let rec repeat t (status : #tac_status as 'a) : 'a = 
+    try repeat t (t status)
+    with NTacStatus.Error _ -> status
+  in
+    atomic_tac (repeat t) s
 ;;
 
-let atomic_tac htac = distribute_tac (exec htac) ;;
 
 let try_tac tac status =
   try
@@ -248,7 +257,7 @@ let first_tac tacl status =
       | Some x -> x
 ;;
 
-let exact_tac t = distribute_tac (fun status goal ->
+let exact_tac t : 's tactic = distribute_tac (fun status goal ->
  let goalty = get_goalty status goal in
  let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
  instantiate status goal t)
@@ -602,13 +611,16 @@ let auto ~params:(l,_) status goal =
         (status, (t,ty) :: l))
       (status,[]) l
   in
-  let pt, metasenv, subst = 
-    Paramod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
-  in      
-  let status = status#set_obj (n,h,metasenv,subst,o) in
-  instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
+  match
+    NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
+  with
+  | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
+  | (pt, metasenv, subst)::_ -> 
+      let status = status#set_obj (n,h,metasenv,subst,o) in
+      instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
 ;;
 
 let auto_tac ~params status =
   distribute_tac (auto ~params) status
 ;;
+