diff options
| -rw-r--r-- | src/Specific/IntegrationTestTemporaryMiscCommon.v | 2 | ||||
| -rw-r--r-- | src/Util/Sigma/Associativity.v | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v index 2cedae976..ab1e821d6 100644 --- a/src/Specific/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v @@ -43,7 +43,7 @@ Ltac eexists_sig_etransitivity := lazymatch goal with | [ |- { a : ?A | @?f a = ?b } ] => let lem := open_constr:(@sig_eq_trans_exist1 A _ f b _) in - simple refine (lem _ _) + simple refine (lem _ (_ : { a : A | _ })) end. Definition sig_R_trans_rewrite_fun_exist1 {B} (R : B -> B -> Prop) {HT : Transitive R} {A} (f : A -> B) (b : B) (f' : A -> B) 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 |