From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 6 Jul 2005 17:20:23 +0000 (+0000)
Subject: Bug fixed: "intros n" should fail when there are less than n products or
X-Git-Tag: V_0_7_1~41
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=df09e8b77a3524441e601bfd3b14ec71ab47b069;p=helm.git

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.
---

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