diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-22 17:05:53 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-22 17:05:53 -0400 |
| commit | e8eba53e187e26f28870e9070360810dbdcbe6b8 (patch) | |
| tree | 7d8db81e63d6721231dd5deb1527ca85d1226c70 /src/Util/Sigma | |
| parent | 9f7c68bbd7c577f79ddfe39640db70b42f813b90 (diff) | |
Fix some minor naming bugs in sig_assoc tactics
Diffstat (limited to 'src/Util/Sigma')
| -rw-r--r-- | src/Util/Sigma/Associativity.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/Util/Sigma/Associativity.v b/src/Util/Sigma/Associativity.v index fbebf2584..005e7ab2d 100644 --- a/src/Util/Sigma/Associativity.v +++ b/src/Util/Sigma/Associativity.v @@ -7,9 +7,11 @@ Ltac sig_sig_assoc := | [ |- { a : ?A | ?P } ] => let P'' := fresh a in let P' := fresh P'' in + let P' := fresh P' in let term := constr:(fun a : A => match P with | P' => ltac:(let v := (eval cbv [P'] in P') in - lazymatch eval pattern (proj1_sig a) in v with + let proj := lazymatch v with context[@proj1_sig ?A ?P a] => constr:(@proj1_sig A P a) end in + lazymatch eval pattern proj in v with | ?P _ => exact P end) end) in |