* @return the new metasenv and the index of the added conjecture *)
val mk_implicit: Cic.metasenv -> Cic.context -> Cic.metasenv * int
+(** as above, but the fresh metavariable represents a type *)
+val mk_implicit_type: Cic.metasenv -> Cic.context -> Cic.metasenv * int
+
+
(** [mk_implicit metasenv context] create n fresh metavariables *)
val n_fresh_metas:
Cic.metasenv -> Cic.context -> int -> Cic.metasenv * Cic.term list
UriManager.uri list ->
Cic.metasenv * (Cic.term Cic.explicit_named_substitution)
-(** as above, but the fresh metavariable represents a type *)
-val mk_implicit_type: Cic.metasenv -> Cic.context -> Cic.metasenv * int
-
val expand_implicits:
Cic.metasenv -> Cic.context -> Cic.term ->
Cic.metasenv * Cic.term