and sort_of_prod subst metasenv context (name,s) (t1, t2) =
let module C = Cic in
+ let context_for_t2 = (Some (name,C.Decl s))::context in
let t1'' = CicMetaSubst.whd subst context t1 in
- let t2'' = CicMetaSubst.whd subst ((Some (name,C.Decl s))::context) t2 in
+ let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
match (t1'', t2'') with
(C.Sort s1, C.Sort s2)
when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
* likely to know the exact value of the result e.g. if the rhs is a
* Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
- CicMkImplicit.mk_implicit metasenv [] in
+ CicMkImplicit.mk_implicit_sort metasenv in
let (subst, metasenv) =
- CicUnification.fo_unif_subst subst context metasenv
+ CicUnification.fo_unif_subst subst context_for_t2 metasenv
(C.Meta (idx,[])) t2''
in
t2'',subst,metasenv
in
let context'' = Some (name, Cic.Decl argty') :: context' in
let (metasenv, idx) =
- CicMkImplicit.mk_implicit metasenv (context'' @ context) in
+ CicMkImplicit.mk_implicit_type metasenv (context'' @ context) in
let irl =
(Some (Cic.Rel 1))::args' @
(CicMkImplicit.identity_relocation_list_for_metavariable ~start:2