-(*CSC: The call to the Intros tactic is embedded inside the code of the *)
-(*CSC: Elim tactic. Do we already need tacticals? *)
-(* Auxiliary function for apply: given a type (a backbone), it returns its *)
-(* head, a META environment in which there is new a META for each hypothesis,*)
-(* a list of arguments for the new applications and the indexes of the first *)
-(* and last new METAs introduced. The nth argument in the list of arguments *)
-(* is the nth new META lambda-abstracted as much as possible. Hence, this *)
-(* functions already provides the behaviour of Intros on the new goals. *)
-let new_metasenv_for_apply_intros proof context ty =
- let module C = Cic in
- let module S = CicSubstitution in
- let rec aux newmeta =
- function
- C.Cast (he,_) -> aux newmeta he
- | C.Prod (name,s,t) ->
- let newcontext,ty',newargument =
- lambda_abstract context newmeta s (fresh_name ())
- in
- let (res,newmetasenv,arguments,lastmeta) =
- aux (newmeta + 1) (S.subst newargument t)
- in
- res,(newmeta,newcontext,ty')::newmetasenv,newargument::arguments,lastmeta
- | t -> t,[],[],newmeta
- in
- let newmeta = new_meta ~proof in
- (* WARNING: here we are using the invariant that above the most *)
- (* recente new_meta() there are no used metas. *)
- let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
- res,newmetasenv,arguments,newmeta,lastmeta
-