Added an implicit parameter to branch_tac to allow branching on a

[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 6011d912d8f7201fa5e20018ca50b619e3625ff3..f5ae3a721e4880a955d4be5463252cf4423e2a36 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -46,13 +46,14 @@ let dot_tac status =
    status#set_stack gstatus
 ;;
 
-let branch_tac status =
+let branch_tac ?(force=false) status =
   let gstatus = 
     match status#stack with
     | [] -> assert false
     | (g, t, k, tag) :: s ->
           match init_pos g with (* TODO *)
-          | [] | [ _ ] -> fail (lazy "too few goals to branch");
+          | [] -> fail (lazy "empty goals")
+         | [_] when (not force) -> fail (lazy "too few goals to branch")
           | loc :: loc_tl ->
                ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
   in
@@ -478,6 +479,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
@@ -586,7 +589,7 @@ let case1_tac name =
              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
-let constructor ?(num=1) ~args status goal = 
+let constructor_tac ?(num=1) ~args = distribute_tac (fun status goal ->
   if num < 1 then fail (lazy "constructor numbers begin with 1");
   let gty = get_goalty status goal in
   let status, (r,_,_,_) = analyse_indty status gty in
@@ -596,11 +599,9 @@ let constructor ?(num=1) ~args status goal =
     Ast.Appl (HExtlib.list_concat ~sep:[Ast.Implicit `Vector]
       ([Ast.NRef ref] :: List.map (fun _,_,x -> [x]) args))
   in
-  exec (apply_tac ("",0,t)) status goal
+  exec (apply_tac ("",0,t)) status goal)
 ;;
 
-let constructor_tac ?num ~args = distribute_tac (constructor ?num ~args);;
-
 let assert0_tac (hyps,concl) = distribute_tac (fun status goal ->
  let gty = get_goalty status goal in
  let eq status ctx t1 t2 =
@@ -644,7 +645,7 @@ let assert_tac seqs status =
        | [seq] -> assert0_tac seq
        | _ ->
          block_tac
-          (branch_tac::
+          ((branch_tac ~force:false)::
           HExtlib.list_concat ~sep:[shift_tac]
             (List.map (fun seq -> [assert0_tac seq]) seqs)@
           [merge_tac])