From a061b4d11fc681182b5bb946aa84d17d0b812225 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 12 Aug 2014 10:17:10 -0400
Subject: Clean up a comment in plugins/romega/ReflOmegaCore

Based on suggestion by @gasche.
---
 plugins/romega/ReflOmegaCore.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index a1308e643b..41b5ec5459 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -980,9 +980,9 @@ Inductive p_step : Set :=
   | P_STEP : step -> p_step
   | P_NOP : p_step.
 
-(* List of normalizations to perform : with a constructor of type
-   [p_step] allowing the visiting of both left and right branches, we would be
-   able to restrict to only one normalization by hypothesis.
+(* List of normalizations to perform : if the type [p_step] had a constructor
+   that indicated visiting both left and right branches, we would be able to
+   restrict ourselves to the case of only one normalization by hypothesis.
    And since all hypothesis are useful (otherwise they wouldn't be included),
    we would be able to replace [h_step] by a simple list. *)
 
-- 
cgit v1.2.3