- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let typ,_ =
- match terms with
- [] -> assert false
- | he::tl ->
- (* We need to check that all the convertibility of all the terms *)
- let u = List.fold_left ( (* TASSI: FIXME *)
- fun u t ->
- let b,u1 = CicReduction.are_convertible context he t u in
- if not b then
- raise AllSelectedTermsMustBeConvertible
- else
- u1) CicUniv.empty_ugraph tl in
- (CicTypeChecker.type_of_aux' metasenv context he u)
+ let uri,metasenv,pbo,pty = proof in
+ let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
+ let subst,metasenv,u,selected_hyps,terms_with_context =
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ~conjecture ~pattern in
+ let context = CicMetaSubst.apply_subst_context subst context in
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
+ let pbo = CicMetaSubst.apply_subst subst pbo in
+ let pty = CicMetaSubst.apply_subst subst pty in
+ let status = (uri,metasenv,pbo,pty),goal in
+ let term =
+ match term with
+ None -> None
+ | Some term ->
+ Some (fun context metasenv ugraph ->
+ let term, metasenv, ugraph = term context metasenv ugraph in
+ CicMetaSubst.apply_subst subst term, metasenv, ugraph)
+ in
+ let u,typ,term, metasenv =
+ let context_of_t, (t, metasenv, u) =
+ match terms_with_context, term with
+ [], None ->
+ raise
+ UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
+ | [], Some t -> context, t context metasenv u
+ | (context_of_t, _)::_, Some t ->
+ context_of_t, t context_of_t metasenv u
+ | (context_of_t, t)::_, None -> context_of_t, (t, metasenv, u)