1 files changed, 12 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 48bfeb86e4..36a297c81e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -130,6 +130,18 @@ let head_constr_bound t =
 let head_constr c =
   try head_constr_bound c with Bound -> error "Bound head variable."
 
+let decompose_app_bound t =
+  let t = strip_outer_cast t in
+  let _,ccl = decompose_prod_assum t in
+  let hd,args = decompose_app_vect ccl in
+  match kind_of_term hd with
+    | Const (c,u) -> ConstRef c, args
+    | Ind (i,u) -> IndRef i, args
+    | Construct (c,u) -> ConstructRef c, args
+    | Var id -> VarRef id, args
+    | Proj (p, c) -> ConstRef p, Array.cons c args
+    | _ -> raise Bound
+
 (******************************************)
 (*           Primitive tactics            *)
 (******************************************)