467
467
let b = detype isgoal avoid env b in
468
468
let id = next_name_away na avoid in
469
469
let avoid = id::avoid and env = add_name (Name id) env in
470
share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c t
470
share_names isgoal n ((Name id,Explicit,Some b,t')::l) avoid env c (lift 1 t)
471
471
(* Only if built with the f/n notation or w/o let-expansion in types *)
472
472
| _, LetIn (_,b,_,t) when n > 0 ->
473
473
share_names isgoal n l avoid env c (subst1 b t)