diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-21 17:27:52 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-21 17:27:52 -0700 |
| commit | aba76c3a9f2ad9f41700519cec67dfc2e2dc285a (patch) | |
| tree | 94e237cf59fdfab6de2cdd9af52353b9b152d6b3 /src/Experiments | |
| parent | 2e91656515d14d4dcdfb352d421ccff87b4d26f0 (diff) | |
Shadowing of ltac constr-bound variables with identifiers is forbidden in 8.5
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |