-let mk_implicit' metasenv context =
- let (metasenv, index) = mk_implicit metasenv context in
- (metasenv, index - 1, index)
-
-let mk_implicit_type metasenv context =
- let newmeta = new_meta metasenv in
- let irl = identity_relocation_list_for_metavariable context in
- ([ newmeta, context, Cic.Sort Cic.Type ;
- newmeta + 1, context, Cic.Meta (newmeta, irl) ] @metasenv,
- newmeta + 1)
-