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/Coqlib.v | 2 -- lib/Floats.v | 1 + lib/Iteration.v | 2 ++ lib/UnionFind.v | 1 + 4 files changed, 4 insertions(+), 2 deletions(-) (limited to 'lib') 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