+let mk_implicit_type metasenv context =
+ let newmeta = new_meta metasenv in
+ ([ newmeta, [], Cic.Sort Cic.Type ;
+ newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
+ newmeta + 1)
+
+let mk_implicit_sort metasenv =
+ let newmeta = new_meta metasenv in
+ ([ newmeta, [], Cic.Sort Cic.Type] @ metasenv, newmeta)
+