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 --- lib/Iteration.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib/Iteration.v') 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]: -- cgit