specialize_by: only specialize arguments of type [Prop]

1 files changed, 7 insertions, 4 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 69e74a3fe..d0c785fed 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -262,10 +262,13 @@ Ltac specialize_by' tac :=
   idtac;
   match goal with
   | [ H : ?A -> ?B |- _ ] =>
-    let H' := fresh in
-    assert (H' : A) by tac;
-    transparent_specialize_one H H';
-    try clear H' (* if [H] was transparent, [H'] will remain *)
+    match type of A with
+      Prop => 
+      let H' := fresh in
+      assert (H' : A) by tac;
+      transparent_specialize_one H H';
+      try clear H' (* if [H] was transparent, [H'] will remain *)
+    end
   end.
 
 Ltac specialize_by tac := repeat specialize_by' tac.