-(* 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 just the nth new META. *)
-let new_metasenv_for_apply newmeta proof context ty =
- let module C = Cic in
- let module S = CicSubstitution in
- let rec aux newmeta =
- function
- C.Cast (he,_) -> aux newmeta he
- (* If the expected type is a Type, then also Set is OK ==>
- * we accept any term of type Type *)
- (*CSC: BUG HERE: in this way it is possible for the term of
- * type Type to be different from a Sort!!! *)
- | C.Prod (name,(C.Sort C.Type as s),t) ->
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- let newargument = C.Meta (newmeta+1,irl) in
- let (res,newmetasenv,arguments,lastmeta) =
- aux (newmeta + 2) (S.subst newargument t)
- in
- res,
- (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv,
- newargument::arguments,lastmeta
- | C.Prod (name,s,t) ->
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- let newargument = C.Meta (newmeta,irl) in
- let (res,newmetasenv,arguments,lastmeta) =
- aux (newmeta + 1) (S.subst newargument t)
- in
- res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta
- | t -> t,[],[],newmeta
- 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,lastmeta
-