+ | NCic.Implicit (`Typeof _) ->
+ (match NCicReduction.whd ~subst context t with
+ NCic.Sort _ -> metasenv,subst,t
+ | NCic.Meta (i,_) when
+ let _,_,ty = NCicUtils.lookup_meta i metasenv in
+ (match ty with
+ NCic.Implicit (`Typeof _) -> true
+ | _ -> false)
+ -> metasenv,subst,t
+ | NCic.Meta (i,_) ->
+ let rec remove_and_hope i =
+ let _,ctx,ty = NCicUtils.lookup_meta i metasenv in
+ match ty with
+ NCic.Implicit _ -> List.filter (fun i',_ -> i <> i') metasenv
+ | _ ->
+ match NCicReduction.whd ~subst ctx ty with
+ NCic.Meta (j,_) ->
+ let metasenv = remove_and_hope j in
+ List.filter (fun i',_ -> i <> i') metasenv
+ | _ -> assert false (* NON POSSO RESTRINGERE *)
+ in
+ let metasenv = remove_and_hope i in
+ let metasenv =
+ (i,(None,[],NCic.Implicit (`Typeof i)))::
+ List.filter (fun i',_ -> i <> i') metasenv
+ in
+ metasenv,subst,t
+ | NCic.Appl (NCic.Meta _::_) ->
+ raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
+ | t when could_reduce t ->
+ raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))
+ | _ ->
+ raise (UnificationFailure (lazy "Trying to instantiate a metavariable that represents a sort with a term")))