(** as above, but the fresh metavariable represents a type *)
val mk_implicit_type: Cic.metasenv -> Cic.context -> Cic.metasenv * int
+(** as above, but the fresh metavariable represents a sort *)
+val mk_implicit_sort: Cic.metasenv -> Cic.metasenv * int
(** [mk_implicit metasenv context] create n fresh metavariables *)
val n_fresh_metas: