- 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,metasenv
+ 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,metasenv