From aba76c3a9f2ad9f41700519cec67dfc2e2dc285a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 21 Jun 2016 17:27:52 -0700 Subject: Shadowing of ltac constr-bound variables with identifiers is forbidden in 8.5 --- src/Experiments/DerivationsOptionRectLetInEncoding.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Experiments') diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index 33fdb5a17..256ceb6b8 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -133,7 +133,7 @@ Proof. unfold iter_op. lazymatch goal with | [ |- ?proj (snd (funexp ?f ?x ?n)) === snd (funexp ?f' _ ?n) ] - => pose proof (fun pf x0 x1 => @funexp_proj _ _ _ _ (fun x => (fst x, proj (snd x))) f f' (Proper_test_and_op (Requiv:=T'Equiv)) pf (x0, x1)) as H'; + => pose proof (fun pf x0 x1 => @funexp_proj _ _ _ _ (fun x' => (fst x', proj (snd x'))) f f' (Proper_test_and_op (Requiv:=T'Equiv)) pf (x0, x1)) as H'; lazymatch type of H' with | ?H'' -> _ => assert (H'') as pf; [clear H'|edestruct (H' pf); simpl in *; solve [eauto]] end @@ -339,4 +339,4 @@ Qed. Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y. Proof. split; eauto using F_eqb_eq, F_eqb_complete. -Qed. \ No newline at end of file +Qed. -- cgit v1.2.3