- (fun cty pbo (i, acc, s, m, ugraph) ->
- (* Pi k_par, (naw_)outty right_par (K_i left_par k_par) *)
- let infty_pbo =
- add_params m s context uri tyno cty outty leftno i in
- let expty_pbo =
- add_params m s context uri tyno cty new_outty leftno i in
+ (fun cty pbo (i, acc, s, menv, ugraph) ->
+ (* Pi k_par, (Pi H:m=(K_i left_par k_par)),
+ * (new_)outty right_par (K_i left_par k_par) *)
+ let infty_pbo, _ =
+ add_params menv s context uri tyno
+ cty outty mty m leftno i in
+ debug_print
+ (lazy ("CASE: infty_pbo: "^CicMetaSubst.ppterm_in_context
+ ~metasenv subst infty_pbo context));
+ let expty_pbo, k = (* k is (K_i left_par k_par) *)
+ add_params menv s context uri tyno
+ cty new_outty mty m leftno i in
+ debug_print
+ (lazy ("CASE: expty_pbo: "^CicMetaSubst.ppterm_in_context
+ ~metasenv subst expty_pbo context));
+ let pbo = add_lambda_for_refl_m pbo rno mty m k cty in
+ debug_print
+ (lazy ("CASE: pbo: " ^ CicMetaSubst.ppterm_in_context
+ ~metasenv subst pbo context));