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