From 6da2ba331f14bccc3ccfa8f75db0b771aba9ffe1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 19 May 2015 11:07:31 -0700
Subject: [PATCH] fix(library/user_recursors): memory access violation

---
 src/library/user_recursors.cpp              |  4 ++++
 tests/lean/user_rec_crash.lean              |  4 ++++
 tests/lean/user_rec_crash.lean.expected.out | 14 ++++++++++++++
 3 files changed, 22 insertions(+)
 create mode 100644 tests/lean/user_rec_crash.lean
 create mode 100644 tests/lean/user_rec_crash.lean.expected.out

diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index ceff1361f..d1879689b 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -100,6 +100,10 @@ recursor_info mk_recursor_info(environment const & env, name const & r, optional
             dep_elim = true;
         else
             dep_elim = false;
+    } else if (C_args.empty()) {
+        throw exception(sstream() << "invalid user defined recursor, '" << r << "' does not support dependent elimination, "
+                        << "and position of the major premise was not specified "
+                        << "(solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)");
     } else {
         major    = C_args.back();
         dep_elim = true;
diff --git a/tests/lean/user_rec_crash.lean b/tests/lean/user_rec_crash.lean
new file mode 100644
index 000000000..80c3f8490
--- /dev/null
+++ b/tests/lean/user_rec_crash.lean
@@ -0,0 +1,4 @@
+example (a b : Prop) (h : a ∧ b) : a :=
+begin
+  induction h using and.rec_on with h₁ h₂,
+end
diff --git a/tests/lean/user_rec_crash.lean.expected.out b/tests/lean/user_rec_crash.lean.expected.out
new file mode 100644
index 000000000..83ea15216
--- /dev/null
+++ b/tests/lean/user_rec_crash.lean.expected.out
@@ -0,0 +1,14 @@
+induction: h and.rec_on (h₁ h₂)
+user_rec_crash.lean:3:2: error:invalid 'induction' tactic, invalid user defined recursor, 'and.rec_on' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor <pos>]', where <pos> is the position of the major premise)
+proof state:
+a b : Prop,
+h : a ∧ b
+⊢ a
+user_rec_crash.lean:4:0: error: don't know how to synthesize placeholder
+a b : Prop,
+h : a ∧ b
+⊢ a
+user_rec_crash.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b : Prop) (h : …),
+    ?M_1