- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- let subst_item = uri,C.Meta (!next_fresh_meta,irl) in
- newmetasenvfragment :=
- (!next_fresh_meta,context,ty)::!newmetasenvfragment ;
- exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
- incr next_fresh_meta ;
- subst_item::(aux (tl,[]))
+ (match ty with
+ C.Sort C.Type as s ->
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let fresh_meta = !next_fresh_meta in
+ let fresh_meta' = fresh_meta + 1 in
+ next_fresh_meta := !next_fresh_meta + 2 ;
+ let subst_item = uri,C.Meta (fresh_meta',irl) in
+ newmetasenvfragment :=
+ (fresh_meta,[],C.Sort C.Type) ::
+ (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;
+ exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
+ subst_item::(aux (tl,[]))
+ | _ ->
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let subst_item = uri,C.Meta (!next_fresh_meta,irl) in
+ newmetasenvfragment :=
+ (!next_fresh_meta,context,ty)::!newmetasenvfragment ;
+ exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
+ incr next_fresh_meta ;
+ subst_item::(aux (tl,[])))