let module C = Cic in
let module S = CicSubstitution in
let rec aux newmeta ty =
- let ty' = (*CicReduction.whd context*) ty in
+ let ty' = ty in
match ty' with
C.Cast (he,_) -> aux newmeta he
(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
let (res,newmetasenv,arguments,lastmeta) =
aux (newmeta + 1) (S.subst newargument t)
in
- res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta
- | t -> t,[],[],newmeta
+ let s' = CicReduction.normalize ~delta:false context s in
+ res,(newmeta,context,s')::newmetasenv,newargument::arguments,lastmeta
+ | t -> (CicReduction.normalize ~delta:false context t),[],[],newmeta
in
(* WARNING: here we are using the invariant that above the most *)
(* recente new_meta() there are no used metas. *)
let termty =
CicSubstitution.subst_vars exp_named_subst_diff termty
in
+ prerr_endline ("term:" ^ CicPp.ppterm term);
+ prerr_endline ("termty:" ^ CicPp.ppterm termty);
let subst,newmetasenv',t =
try
new_metasenv_and_unify_and_t newmeta' metasenv' proof context term' ty
in
let bo' = apply_subst t in
let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
+(* prerr_endline ("me: " ^ CicMetaSubst.ppmetasenv newmetasenv'' subst); *)
let subst_in =
(* if we just apply the subtitution, the type is irrelevant:
we may use Implicit, since it will be dropped *)