- let selected_hyps,terms_with_context =
- ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
- let typ,term =
- match terms_with_context, term with
- [], None ->
- raise UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
- | _, Some term
- | (_,term)::_, None ->
- fst
- (CicTypeChecker.type_of_aux' metasenv context term
- CicUniv.empty_ugraph),
- term 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 (CicMetaSubst.apply_subst subst term) in
+ let u,typ,term =
+ let context_of_t,t =
+ match terms_with_context, term with
+ [], None ->
+ raise
+ UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
+ | _, Some t -> context,t
+ | (context_of_t,t)::_, None -> context_of_t,t
+ in
+ let t,subst,metasenv' =
+ try
+ CicMetaSubst.delift_rels [] metasenv
+ (List.length context_of_t - List.length context) t
+ with
+ CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable ->
+ raise TheSelectedTermsMustLiveInTheGoalContext in
+ (*CSC: I am not sure about the following two assertions;
+ maybe I need to propagate the new subst and metasenv *)
+ assert (subst = []);
+ assert (metasenv' = metasenv);
+ let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in
+ u,typ,t
+ in