- match terms_with_context, term with
- [], None ->
- raise UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly
- | _, Some term
- | (_,term)::_, None ->
- let typ,u =
- CicTypeChecker.type_of_aux' ~subst metasenv context term u
- in
- 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