in
(context',ty,C.LetIn(n,s,bo))
| _ as t ->
- let irl =
+ if howmany <= 0 then
+ let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
- in
- context, t, (C.Meta (newmeta,irl))
+ in
+ context, t, (C.Meta (newmeta,irl))
+ else
+ raise (Fail "intro(s): not enough products or let-ins")
in
collect_context context howmany ty