- (fun (subst,metasenv) (instance,args) ->
- let instance' =
- CicReduction.whd context (C.Appl(outtype::args)) in
+ (fun (subst,metasenv) (constructor_args_no,context,instance,args) ->
+ let instance' =
+ let appl =
+ let outtype' =
+ CicSubstitution.lift constructor_args_no outtype
+ in
+ C.Appl (outtype'::args)
+ in
+(*
+ (* if appl is not well typed then the type_of below solves the
+ * problem *)
+ let (_, subst, metasenv) =
+ type_of_aux subst metasenv context appl
+ in
+*)
+ CicMetaSubst.whd subst context appl
+ in