From e8eba53e187e26f28870e9070360810dbdcbe6b8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 22 Jun 2017 17:05:53 -0400 Subject: Fix some minor naming bugs in sig_assoc tactics --- src/Util/Sigma/Associativity.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'src/Util/Sigma') 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 -- cgit v1.2.3