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 + common/Linking.v | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'common') 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 *) diff --git a/common/Linking.v b/common/Linking.v index 089f4fd2..d23b1028 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -869,7 +869,7 @@ Infix ":::" := pass_cons (at level 60, right associativity) : linking_scope. Fixpoint compose_passes (l l': Language) (passes: Passes l l') : Pass l l' := match passes in Passes l l' return Pass l l' with | pass_nil l => pass_identity l - | pass_cons l1 l2 l3 pass1 passes => pass_compose pass1 (compose_passes passes) + | pass_cons pass1 passes => pass_compose pass1 (compose_passes passes) end. (** Some more lemmas about [nlist_forall2]. *) -- cgit