X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=fc0a8013cca3b09deb1b8ab9703499dc0f66d4f5;hb=e34ae2f76136c6c381826b81407e9cacebb7cfd4;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..fc0a8013c 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -179,17 +179,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,7 +225,7 @@ 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 = distribute_tac (exec htac) ;;
@@ -248,7 +247,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)