- let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+ begin
+ match sort with
+ Cic.Sort _
+ (* instead of raising Uncertain, let's hope that the meta will become
+ a sort *)
+ | Cic.Meta _ -> ()
+ | _ -> raise (RefineFailure "The term provided is not a type")
+ end;