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 --- backend/Inlining.v | 7 +++++-- cfrontend/Ctypes.v | 2 ++ common/Behaviors.v | 1 + common/Linking.v | 2 +- lib/Coqlib.v | 2 -- lib/Floats.v | 1 + lib/Iteration.v | 2 ++ lib/UnionFind.v | 1 + 8 files changed, 13 insertions(+), 5 deletions(-) diff --git a/backend/Inlining.v b/backend/Inlining.v index 7eb0f0fa..d66d2586 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -293,10 +293,13 @@ Inductive inline_decision (ros: reg + ident) : Type := | Cannot_inline | Can_inline (id: ident) (f: function) (P: ros = inr reg id) (Q: fenv!id = Some f). +Arguments Cannot_inline {ros}. +Arguments Can_inline {ros}. + Program Definition can_inline (ros: reg + ident): inline_decision ros := match ros with - | inl r => Cannot_inline _ - | inr id => match fenv!id with Some f => Can_inline _ id f _ _ | None => Cannot_inline _ end + | inl r => Cannot_inline + | inr id => match fenv!id with Some f => Can_inline id f _ _ | None => Cannot_inline end end. (** Inlining of a call to function [f]. An appropriate context is diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 7b2c7354..e3356510 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -20,6 +20,8 @@ Require Import Axioms Coqlib Maps Errors. Require Import AST Linking. Require Archi. +Set Asymmetric Patterns. + Local Open Scope error_monad_scope. (** * Syntax of types *) 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]. *) diff --git a/lib/Coqlib.v b/lib/Coqlib.v index c023bdd5..045fb03a 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -25,8 +25,6 @@ Require Export List. Require Export Bool. Require Export Lia. -Global Set Asymmetric Patterns. - (** * Useful tactics *) Ltac inv H := inversion H; clear H; subst. diff --git a/lib/Floats.v b/lib/Floats.v index f56078aa..43caebb0 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -26,6 +26,7 @@ Import ListNotations. Close Scope R_scope. Open Scope Z_scope. +Set Asymmetric Patterns. Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *) Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *) diff --git a/lib/Iteration.v b/lib/Iteration.v index 82110bff..66bb3970 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -20,6 +20,8 @@ Require Import Axioms. Require Import Coqlib. Require Import Wfsimpl. +Set Asymmetric Patterns. + (** This modules defines several Coq encodings of a general "while" loop. The loop is presented in functional style as the iteration of a [step] function of type [A -> B + A]: diff --git a/lib/UnionFind.v b/lib/UnionFind.v index 67e4271d..1bc2f657 100644 --- a/lib/UnionFind.v +++ b/lib/UnionFind.v @@ -21,6 +21,7 @@ Require Import Coqlib. Open Scope nat_scope. Set Implicit Arguments. +Set Asymmetric Patterns. (* To avoid useless definitions of inductors in extracted code. *) Local Unset Elimination Schemes. -- cgit