From 9f7ff19fe178823bf94ec532fbdf4e9fa2bfcfa6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 9 Oct 2016 17:37:55 -0400 Subject: Fix compatibility with sigT notation --- src/ModularArithmetic/ModularBaseSystemOpt.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 3eef0901e..d1bd49a55 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -264,7 +264,7 @@ Section Carries. eexists. intros H. rewrite <-carry_gen_opt_correct by assumption. cbv beta iota delta [carry_gen_opt]. - match goal with |- appcontext[?a & Z_ones_opt _] => + match goal with |- appcontext[?a &' Z_ones_opt _] => let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in let RHSf := match (eval pattern (a) in RHS) with ?RHSf _ => RHSf end in -- cgit v1.2.3