new intro:

[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 f6d8bfaec3055f456c70615207ed3fc74f98aa8b..f3d74050f9247cb07cc14d231428c5108ba683da 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -556,6 +556,25 @@ let intro_tac name =
     if name = "_" then clear_tac [name] else id_tac ]
 ;;
 
+let name_counter = ref 0;;
+let intros_tac ?names_ref names s =
+  let names_ref, prefix = 
+    match names_ref with | None -> ref [], "__" | Some r -> r, "H" 
+  in
+  if names = [] then
+   repeat_tac 
+     (fun s ->
+        incr name_counter;
+        (* TODO: generate better names *)
+        let name = prefix ^ string_of_int !name_counter in
+        let s = intro_tac name s in 
+        names_ref := !names_ref @ [name];
+        s)
+     s
+   else
+     block_tac (List.map intro_tac names) s
+;;
+
 let cases ~what status goal =
  let gty = get_goalty status goal in
  let status, what = disambiguate status (ctx_of gty) what None in