From b6fb5a567c1d3d0bbe1f30e875d2cdcaba9514ad Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 12 Jun 2020 18:40:42 +0100
Subject: Coq: fix matching bug in solver

---
 lib/coq/Values.v | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Values.v b/lib/coq/Values.v
index b0d08670..256d7c19 100644
--- a/lib/coq/Values.v
+++ b/lib/coq/Values.v
@@ -2109,10 +2109,13 @@ Ltac squashed_andor_solver :=
     destruct H as [x H'];
     exists x
   end;
-  (* Attempt to shrink size of problem *)
+  (* Attempt to shrink size of problem.
+     I originally used just one match here with a non-linear pattern, but it
+     appears it matched up to convertability and so definitions could break
+     the generalization. *)
   try match goal with
-      | _ : l = _ -> ?v = r |- context[?v] => generalize dependent v; intros
-      | _ : l = _ -> Bool.eqb ?v r = true |- context[?v] => generalize dependent v; intros
+      | _ : l = _ -> ?v = r |- _ => match goal with |- context[v] => generalize dependent v; intros end
+      | _ : l = _ -> Bool.eqb ?v r = true |- _ => match goal with |- context[v] => generalize dependent v; intros end
       end;
   unbool_comparisons; unbool_comparisons_goal;
   repeat match goal with
-- 
cgit v1.2.3