From c48ade3f0d6324872d292932e797ffd718ad57d9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 7 Aug 2014 12:24:29 +0200 Subject: A couple of fixes/improvements in -beautify, but backtracking on change of printing format of forall (need more thinking). --- theories/Relations/Operators_Properties.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index c2cd9628b..cf1aa9baf 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -35,7 +35,8 @@ Section Properties. Section Clos_Refl_Trans. - Local Notation "R *" := (clos_refl_trans R) (at level 8, left associativity). + Local Notation "R *" := (clos_refl_trans R) + (at level 8, left associativity, format "R *"). (** Correctness of the reflexive-transitive closure operator *) -- cgit v1.2.3