- let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
- let (subst, metasenv,ugraph1) =
- try
- fo_unif_subst subst context metasenv hetype hetype' ugraph
- with exn ->
- enrich localization_tbl he
- ~f:(fun _ ->
- (lazy ("The term " ^
- CicMetaSubst.ppterm_in_context subst he
- context ^ " (that has type " ^
- CicMetaSubst.ppterm_in_context subst hetype
- context ^ ") is here applied to " ^
- string_of_int (List.length tlbody_and_type) ^
- " arguments that are more than expected"
- (* "\nReason: " ^ Lazy.force exn*)))) exn
+ let ((subst,metasenv,ugraph1),hetype') =
+ if CicUtil.is_meta_closed hetype then
+ (subst,metasenv,ugraph),hetype
+ else
+ let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
+ try
+ fo_unif_subst_eat_prods subst context metasenv hetype hetype' ugraph, hetype'
+ with exn ->
+ enrich localization_tbl he
+ ~f:(fun _ ->
+ (lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context subst he
+ context ^ " (that has type " ^
+ CicMetaSubst.ppterm_in_context subst hetype
+ context ^ ") is here applied to " ^
+ string_of_int (List.length tlbody_and_type) ^
+ " arguments that are more than expected"
+ (* "\nReason: " ^ Lazy.force exn*)))) exn