- Used in CicRefine.sort_of_prod.
(** 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:
* likely to know the exact value of the result e.g. if the rhs is a
* Sort (Prop | Set | CProp) then the result is the rhs *)
let (metasenv,idx) =
- CicMkImplicit.mk_implicit metasenv [] in
+ CicMkImplicit.mk_implicit_sort metasenv in
let (subst, metasenv) =
CicUnification.fo_unif_subst subst context_for_t2 metasenv
(C.Meta (idx,[])) t2''