From df09e8b77a3524441e601bfd3b14ec71ab47b069 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 6 Jul 2005 17:20:23 +0000 Subject: [PATCH] Bug fixed: "intros n" should fail when there are less than n products or let-ins. In particular "intro" should fail if the goal is not a product or a let-in. --- helm/ocaml/tactics/primitiveTactics.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 06e83a125..1b5f407bc 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -61,10 +61,13 @@ let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name = 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 -- 2.39.2