From 4c1f3132fc077c2e33ec94f20674e7c4cf714f68 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 8 Nov 2017 01:45:55 -0500 Subject: Fix another side condition issue --- src/Arithmetic/Saturated/Freeze.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Arithmetic') diff --git a/src/Arithmetic/Saturated/Freeze.v b/src/Arithmetic/Saturated/Freeze.v index 7c05084f6..78a86bc73 100644 --- a/src/Arithmetic/Saturated/Freeze.v +++ b/src/Arithmetic/Saturated/Freeze.v @@ -126,7 +126,7 @@ End Freeze. Hint Opaque freeze_cps : uncps. Hint Rewrite @freeze_id : uncps. Hint Rewrite @eval_freeze - using (assumption || auto) : push_basesystem_eval. + using (assumption || reflexivity || auto || eassumption || omega) : push_basesystem_eval. Hint Unfold freeze freeze_cps -- cgit v1.2.3