exception WrongUriToConstant of string
exception WrongUriToVariable of string
exception WrongUriToMutualInductiveDefinitions of string
-exception MutCaseFixAndCofixRefineNotImplemented;;
(* type_of_aux' metasenv context term *)
(* refines [term] and returns the refined form of [term], *)