+ (proof, goal), List.length terms
+;;
+
+let compose_tac ?howmany ?mk_fresh_name_callback n t1 t2 proofstatus =
+ let ((proof, goal), k), n =
+ match t2 with
+ | Some t2 -> compose_core t1 t2 proofstatus, n-1
+ | None ->
+ let k =
+ let proof, goal = proofstatus in
+ let _,metasenv,subst,_,_,_ = proof in
+ let _,_,ty = CicUtil.lookup_meta goal metasenv in
+ count_pi (CicMetaSubst.apply_subst subst ty)
+ in
+ (proofstatus, k), n
+ in
+ let (proof, goal), k =
+ (* fix iterates n times the composition *)
+ let rec fix proofstatus k t = function
+ | 0 -> proofstatus, k
+ | n ->
+ let t = CicSubstitution.lift k t in
+ let proof, gl =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.intros_tac
+ ~howmany:k ?mk_fresh_name_callback ()) proofstatus
+ in
+ assert (List.length gl = 1);
+ let goal = List.hd gl in
+ let k, proofstatus =
+ (* aux compose t with every previous result *)
+ let rec aux k proofstatus = function
+ | 0 -> k, proofstatus
+ | n ->
+ let (proof, goal), k1 =
+ compose_core t (Cic.Rel n) proofstatus
+ in
+ aux (k+k1) (proof, goal) (n-1)
+ in
+ aux 0 (proof, goal) k
+ in
+ fix proofstatus k t (n-1)
+ in
+ fix (proof, goal) k t1 n
+ in
+ let howmany =
+ match howmany with
+ | None -> None
+ | Some i ->
+ if i - k < 0 then (* we should generalize back and clear *) Some 0
+ else Some (i - k)
+ in
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.intros_tac ?howmany ?mk_fresh_name_callback ())
+ (proof,goal)