From dfd995846be8f0df3162f7ee26cb95d5cc96b251 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 26 Oct 2021 12:02:23 -0700 Subject: [PATCH] GhostSimulations:Be more robust to generated names Fixes #130 ; see #130 for more details Ideally we'd have a way to find and fix all instances like this at once. --- core/GhostSimulations.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/core/GhostSimulations.v b/core/GhostSimulations.v index 4ae7fe4e..38fcd88d 100644 --- a/core/GhostSimulations.v +++ b/core/GhostSimulations.v @@ -83,7 +83,7 @@ Definition deghost (net : @network _ refined_multi_params) : (@network _ multi_p _ ). intros. - destruct net. + destruct net as [? nwState]. concludes. destruct nwState. auto. Defined. @@ -249,7 +249,7 @@ Definition reghost (net : @network _ multi_params) : @network _ refined_multi_pa _ ). intros. - destruct net. + destruct net as [? nwState]. concludes. exact (ghost_init, nwState). Defined.