constructor accepts the arguments of the constructor...

[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 caa069a0d839697cdbfc36e8a0c155bccfed1b3c..b3f05293fac8e03795ecb629fe8f7f67ec005246 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -435,12 +435,8 @@ let letin_tac ~where ~what:(_,_,w) name =
 ;;
 
 let apply_tac (s,n,t) = 
-  let t = 
-    match t with
-    | Ast.AttributedTerm (_,Ast.Binder _) | Ast.Binder _ -> t
-    | _ -> Ast.Appl [t; Ast.Implicit `Vector]
-  in
-    exact_tac (s,n,t)
+  let t = Ast.Appl [t; Ast.Implicit `Vector] in
+  exact_tac (s,n,t)
 ;;
 
 type indtyinfo = {
@@ -577,6 +573,21 @@ let case1_tac name =
              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
 ;;
 
+let constructor ?(num=1) ~args 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
+  let ref = NReference.mk_constructor num r in
+  let t = 
+    if args = [] then Ast.NRef ref else
+    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
+;;
+
+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 =