aboutsummaryrefslogtreecommitdiffstats
path: root/src/versions/standard/Tactics_standard.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/versions/standard/Tactics_standard.v')
-rw-r--r--src/versions/standard/Tactics_standard.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v
index 232ae54..61e663a 100644
--- a/src/versions/standard/Tactics_standard.v
+++ b/src/versions/standard/Tactics_standard.v
@@ -23,7 +23,7 @@ Ltac get_hyps_acc acc k :=
match goal with
| [ H : ?P |- _ ] =>
let T := type of P in
- match T with
+ lazymatch T with
| Prop =>
lazymatch P with
| id _ => fail