aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3881.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/3881.v')
-rw-r--r--test-suite/bugs/closed/3881.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
index 070d1e9c7..a327bbf2a 100644
--- a/test-suite/bugs/closed/3881.v
+++ b/test-suite/bugs/closed/3881.v
@@ -23,7 +23,7 @@ Proof.
pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H
(fun b => ap g (eisretr f b))) as k.
revert k.
- let x := match goal with |- let k := ?x in _ => constr:x end in
+ let x := match goal with |- let k := ?x in _ => constr:(x) end in
intro k; clear k;
pose (x _).
pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _