fix(builtin/tactic): more meaningful error message when skip tactic is used in a full proof

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/tactic.lua

@@ -31,15 +31,15 @@ tactic_macro("simp", { macro_arg.Ids },
 -- This tactic is useful for momentarily ignoring/skipping a "hole" in a big proof.
 -- Remark: the kernel will not accept a proof built using this tactic.
 skip_tac = tactic(function (env, ios, s)
-                     local gs      = s:goals()
+                     local gs       = s:goals()
-                     local pb      = s:proof_builder()
+                     local pb       = s:proof_builder()
-                     local trivial = mk_constant("trivial")
+                     local buggy_pr = mk_constant("invalid proof built using skip tactic")
-                     local new_pb  =
+                     local new_pb   =
                         function(m, a)
                            -- We provide a "fake/incorrect" proof for all goals in gs
                            local new_m = proof_map(m) -- Copy proof map m
                            for n, g in gs:pairs() do
-                              new_m:insert(n, trivial)
+                              new_m:insert(n, buggy_pr)
                            end
                            return pb(new_m, a)
                         end

tests/lean/jbug1.lean

@@ -0,0 +1,12 @@
+import macros
+import tactic
+
+theorem le_iff (a b : Nat) : a ≤ b ↔ a < b ∨ a = b
+:=
+  iff_intro (
+    assume H : a ≤ b,
+    show a < b ∨ a = b, by skip
+  )(
+    assume H : a < b ∨ a = b,
+    show a ≤ b, by skip
+  )

tests/lean/jbug1.lean.expected.out

@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'macros'
+  Imported 'tactic'
+jbug1.lean:4:0: error: unknown object 'invalid proof built using skip tactic'