diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-05 02:49:36 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-05 02:49:36 -0400 |
commit | fa5c6aed76360c188ac097259b774ba32129aecb (patch) | |
tree | fddda01ee54b9b5e197805be24ec3d233f75182a /src/Util | |
parent | 3125b2c088cb33d5b029e74a7b938e25afc9a304 (diff) |
Fix bug in change_with_curried
Comes from unfortunate behavior of [change x with y in *]
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Curry.v | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/Util/Curry.v b/src/Util/Curry.v index 6d15eca05..8a34cb611 100644 --- a/src/Util/Curry.v +++ b/src/Util/Curry.v @@ -1,6 +1,14 @@ Definition curry2 {A B C} (f : A -> B -> C) (x : A * B) : C := let '(a, b) := x in f a b. +(** Work around "Cannot create self-referring hypothesis" coming from + [change x with y in *] *) +Local Ltac change_in_all from to := + change from with to; + repeat match goal with + | [ H : _ |- _ ] => progress change from with to in H + end. + Ltac change_with_curried f := cbv beta in f; (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=5430 *) lazymatch type of f with @@ -8,7 +16,7 @@ Ltac change_with_curried f := => let f' := fresh f in rename f into f'; pose (fun (ab : A * B) => f' (fst ab) (snd ab)) as f; - change f' with (fun (a : A) (b : B) => f (a, b)) in *; + change_in_all f' (fun (a : A) (b : B) => f (a, b)); subst f'; cbv beta; change_with_curried f |