diff options
Diffstat (limited to 'plugins/romega/ReflOmegaCore.v')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index ab424c22..b84cf254 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 to visit 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. *) @@ -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] *) @@ -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. @@ -1284,7 +1284,7 @@ Qed. (* Extraire une hypothèse de la liste *) Definition nth_hyps (n : nat) (l : hyps) := nth n l TrueTerm. - +Unset Printing Notations. Theorem nth_valid : forall (ep : list Prop) (e : list int) (i : nat) (l : hyps), interp_hyps ep e l -> interp_proposition ep e (nth_hyps i l). |