| Some (n,Cic.Def (s,None)) ->
Some (n,Cic.Def ((subst_in canonical_context' s),None))
| None -> None
- | Some (_,Cic.Def (_,Some _)) -> assert false
+ | Some (n,Cic.Def (bo,Some ty)) ->
+ Some
+ (n,
+ Cic.Def
+ (subst_in canonical_context' bo,
+ Some (subst_in canonical_context' ty)))
in
entry'::canonical_context'
) canonical_context []
in
C.Appl (eliminator_ref :: make_tl term (args_no - 1))
in
- let metasenv', term_to_refine' =
- CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in
let refined_term,_,metasenv'',_ =
- CicRefine.type_of_aux' metasenv' context term_to_refine'
+ CicRefine.type_of_aux' metasenv' context term_to_refine
CicUniv.empty_ugraph
in
let new_goals =