let-ins. In particular "intro" should fail if the goal is not a product or
a let-in.
in
(context',ty,C.LetIn(n,s,bo))
| _ as t ->
in
(context',ty,C.LetIn(n,s,bo))
| _ as t ->
+ if howmany <= 0 then
+ let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context
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
in
collect_context context howmany ty