X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=10fa168d492517123eff7b4b18861cb9827cfa47;hb=d97886196d2c730f72312b226bebc388be08f39e;hp=d366c87d233660634c2da5c3a510c051d331e280;hpb=01304bffd3ee2a66216214a9e1a8ee7fdfdf16e3;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index d366c87d2..10fa168d4 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -52,7 +52,7 @@ let branch_tac status =
     | [] -> assert false
     | (g, t, k, tag) :: s ->
           match init_pos g with (* TODO *)
-          | [] | [ _ ] -> fail (lazy "too few goals to branch");
+          | [] | [ _ ] -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->
                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
   in
@@ -478,6 +478,8 @@ type indtyinfo = {
  }
 ;;
 
+let ref_of_indtyinfo iti = iti.reference;;
+
 let analyze_indty_tac ~what indtyref =
  distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in