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 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'backend') 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 -- cgit