diff options
| author |  Jason Gross <jgross@mit.edu> | 2014-08-12 10:17:10 -0400 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-08-25 15:22:40 +0200 |
| commit | a061b4d11fc681182b5bb946aa84d17d0b812225 (patch) | |
| tree | 2e986623a7803f8a716dacd8e1773075126b093b /plugins/romega/ReflOmegaCore.v | |
| parent | 82312ad28ea14203cbfae9a7f69d2b8ab23c6b9f (diff) | |
Clean up a comment in plugins/romega/ReflOmegaCore
Based on suggestion by @gasche.
Diffstat (limited to 'plugins/romega/ReflOmegaCore.v')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index a1308e643..41b5ec545 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. *) |