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 06e83a125335ea218df3a3e25f2c02f197910397..1b5f407bc31c2cdfddd5814c7346dc5c64b5a6b0 100644 (file)
--- 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