diff --git a/src/library/tactic/destruct_tactic.cpp b/src/library/tactic/destruct_tactic.cpp
index 6be1431483..4153c5a039 100644
--- a/src/library/tactic/destruct_tactic.cpp
+++ b/src/library/tactic/destruct_tactic.cpp
@@ -57,10 +57,15 @@ tactic_state destruct(transparency_mode md, expr const & e, tactic_state const &
 
     expr cases;
     levels lvls;
-    if (env.get(name(I_name, "rec")).get_num_univ_params() != length(I_lvls))
+    if (env.get(name(I_name, "rec")).get_num_univ_params() != length(I_lvls)) {
         lvls = cons(target_lvl, I_lvls);
-    else
+    } else {
+        if (!is_zero(target_lvl)) {
+            throw exception(sstream() << "destruct tactic failed, recursor '" << cases_on_decl.get_name()
+                            << "' can only eliminate into Prop");
+        }
         lvls = I_lvls;
+    }
 
     /* cases will contain the cases_on application that we will assing to the main goal */
     cases                     = mk_constant(cases_on_decl.get_name(), lvls);
diff --git a/tests/lean/1766.lean b/tests/lean/1766.lean
new file mode 100644
index 0000000000..6a0bca5328
--- /dev/null
+++ b/tests/lean/1766.lean
@@ -0,0 +1,32 @@
+inductive is_some (x : option nat) : Prop
+  | mk : ∀ value : nat, x = some value → is_some
+
+def value_1 (x : option nat) (H : is_some x)
+   : nat :=
+begin
+   destruct x; intros,
+   {destruct H, -- ERROR: `is_some` can only eliminate into Prop
+    intros, clear a_2, rw a at a_1, contradiction},
+   {assumption}
+end
+
+def value_2 (x : option nat) (H : is_some x)
+   : x = x :=
+begin
+   destruct x; intros,
+   {destruct H,
+    intros, rw a at a_1},
+   {refl}
+end
+
+inductive is_some' (x : option nat) : Type
+  | mk : ∀ value : nat, x = some value → is_some'
+
+def value_3 (x : option nat) (H : is_some' x)
+   : nat :=
+begin
+   destruct x; intros,
+   {destruct H,
+    intros, clear a_2, rw a at a_1, contradiction},
+   {assumption}
+end
diff --git a/tests/lean/1766.lean.expected.out b/tests/lean/1766.lean.expected.out
new file mode 100644
index 0000000000..2b194362e7
--- /dev/null
+++ b/tests/lean/1766.lean.expected.out
@@ -0,0 +1,6 @@
+1766.lean:8:4: error: destruct tactic failed, recursor 'is_some.cases_on' can only eliminate into Prop
+state:
+x : option ℕ,
+H : is_some x,
+a : x = none
+⊢ ℕ