- let sort2,subst''',metasenv''' =
- type_of_aux subst'' metasenv''((Some (n,(C.Decl s)))::context) type2
- in
- (* only to check if the product is well-typed *)
- let _,subst'''',metasenv'''' =
- sort_of_prod subst''' metasenv''' context (n,s) (sort1,sort2)
- in
- C.Prod (n,s,type2),subst'''',metasenv''''
+ C.Prod (n,s,type2),subst'',metasenv''