diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/README | 2 | ||||
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/README b/plugins/extraction/README index 64c871fd3f..a9a7b04d52 100644 --- a/plugins/extraction/README +++ b/plugins/extraction/README @@ -6,7 +6,7 @@ What is it ? ------------ -The extraction is a mechanism allowing to produce functional code +The extraction is a mechanism that produces functional code (Ocaml/Haskell/Scheme) out of any Coq terms (either programs or proofs). diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 7e4475d401..a1308e643b 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. |