diff options
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 7e4475d40..a1308e643 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -981,7 +981,7 @@ Inductive p_step : Set := | P_NOP : p_step. (* List of normalizations to perform : with a constructor of type - [p_step] allowing to visit both left and right branches, we would be + [p_step] allowing the visiting of both left and right branches, we would be able to restrict to 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. *) @@ -1014,7 +1014,7 @@ Inductive e_step : Set := (* For each reified data-type, we define an efficient equality test. It is not the one produced by [Decide Equality]. - Then we prove two theorem allowing to eliminate such equalities : + Then we prove two theorem allowing elimination of such equalities : \begin{verbatim} (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2. (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2. |