diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/3286.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/3286.v')
-rw-r--r-- | test-suite/bugs/closed/3286.v | 41 |
1 files changed, 41 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v new file mode 100644 index 00000000..b08b7ab3 --- /dev/null +++ b/test-suite/bugs/closed/3286.v @@ -0,0 +1,41 @@ +Require Import FunctionalExtensionality. + +Ltac make_apply_under_binders_in lem H := + let tac := make_apply_under_binders_in in + match type of H with + | forall x : ?T, @?P x + => let ret := constr:(fun x' : T => + let Hx := H x' in + $(let ret' := tac lem Hx in + exact ret')$) in + match eval cbv zeta in ret with + | fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in + constr:(Some P') + end + | _ => let ret := constr:($(match goal with + | _ => (let H' := fresh in + pose H as H'; + apply lem in H'; + exact (Some H')) + | _ => exact (@None nat) + end + )$) in + let ret' := (eval cbv beta zeta in ret) in + constr:(ret') + | _ => constr:(@None nat) + end. + +Ltac apply_under_binders_in lem H := + let H' := make_apply_under_binders_in lem H in + let H'0 := match H' with Some ?H'0 => constr:(H'0) end in + let H'' := fresh in + pose proof H'0 as H''; + clear H; + rename H'' into H. + +Goal forall A B C (f g : forall (x : A) (y : B x), C x y), (forall x y, f x y = g x y) -> True. +Proof. + intros A B C f g H. + let lem := constr:(@functional_extensionality_dep) in + apply_under_binders_in lem H. +(* Anomaly: Uncaught exception Not_found(_). Please report. *) |