From 613d99b98d3c78213a69acdbf23c660764487300 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 11 Apr 2016 16:09:53 +0200
Subject: Changing rule for "*" in Operator_Properties so that, iterated, it
 does not print to ** which is a keyword.

---
 theories/Relations/Operators_Properties.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 220cebeace..fe8a96acc7 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -36,7 +36,7 @@ Section Properties.
   Section Clos_Refl_Trans.
 
     Local Notation "R *" := (clos_refl_trans R)
-      (at level 8, left associativity, format "R *").
+      (at level 8, no associativity, format "R *").
 
     (** Correctness of the reflexive-transitive closure operator *)
 
-- 
cgit v1.2.3