* Moreover the inferred type is closer to the expected one.
*)
C.LetIn (n,s',t'),CicSubstitution.subst s' inferredty,
- subst',metasenv',ugraph2
+ subst'',metasenv'',ugraph2
| C.Appl (he::((_::_) as tl)) ->
let he',hetype,subst',metasenv',ugraph1 =
type_of_aux subst metasenv context he ugraph
assert (metasenv' = metasenv);
(* Here we do not check the metasenv for correctness *)
let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
- 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;
let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
let bo' = CicMetaSubst.apply_subst subst bo' in
let ty' = CicMetaSubst.apply_subst subst ty' in
let t = CicSubstitution.subst t' t in
i - 1,t
) tys (typesno - 1,t)) in
- let ty' = undebrujin ty in
+ let ty' = undebrujin ty' in
metasenv,ugraph,(name,ty')::res
) cl (metasenv,ugraph,[])
in