From c9fad7cd7bdc4e79fb06a1d39abfa0d5471623e5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 15 Sep 2021 14:00:41 +0200 Subject: Avoid `Global Set Asymmetric Patterns` (#408) Instead, add `Set Asymmetric Patterns` to the files that need it, or use `Arguments` to make inductive types work better with symmetric patterns. Closes: #403 --- common/Behaviors.v | 1 + 1 file changed, 1 insertion(+) (limited to 'common/Behaviors.v') diff --git a/common/Behaviors.v b/common/Behaviors.v index 023b33e2..1f7f6226 100644 --- a/common/Behaviors.v +++ b/common/Behaviors.v @@ -25,6 +25,7 @@ Require Import Integers. Require Import Smallstep. Set Implicit Arguments. +Set Asymmetric Patterns. (** * Behaviors for program executions *) -- cgit