diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 2 | ||||
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 9b72c3e9f..3f5443e03 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -796,7 +796,7 @@ let branch_as_cst (l,_,c) = When searching for the best factorisation below, we'll try both. *) -(* The following structure allows to record which element occurred +(* The following structure allows recording which element occurred at what position, and then finally return the most frequent element and its positions. *) diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 41b5ec545..b84cf2540 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -990,7 +990,7 @@ Inductive h_step : Set := pair_step : nat -> p_step -> h_step. (* \subsubsection{Rules for decomposing the hypothesis} *) -(* This type allows to navigate in the logical constructors that +(* This type allows navigation in the logical constructors that form the predicats of the hypothesis in order to decompose them. This allows in particular to extract one hypothesis from a conjunction with possibly the right level of negations. *) @@ -1000,7 +1000,7 @@ Inductive direction : Set := | D_right : direction | D_mono : direction. -(* This type allows to extract useful components from hypothesis, either +(* This type allows extracting useful components from hypothesis, either hypothesis generated by splitting a disjonction, or equations. The last constructor indicates how to solve the obtained system via the use of the trace type of Omega [t_omega] *) |