- | C.CurrentProof (_,_,te,ty) ->
- (*CSC [] wrong *)
- let _ = type_of ty in
- debug (type_of te) [] ;
- if not (R.are_convertible (type_of te) ty) then
- raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
+ | C.CurrentProof (_,conjs,te,ty) ->
+ (*CSC [] wrong *)
+ let _ = type_of_aux' conjs [] ty in
+ debug (type_of_aux' conjs [] te) [] ;
+ if not (R.are_convertible (type_of_aux' conjs [] te) ty) then
+ raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))