diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-09 13:53:08 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:08:31 +0200 |
| commit | 102494641b9b6c31495bd02ae8c565249fb128b3 (patch) | |
| tree | eefa81f4300e224969b6c1e483090ae8c7eddacb /plugins/romega | |
| parent | 348882636804297e1190e3e1549fa089e4fa8c23 (diff) | |
ReflOmegaCore: discard useless cosntructor P_NOP
Diffstat (limited to 'plugins/romega')
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 5fa40f46f..60c0018c5 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -941,8 +941,7 @@ Inductive p_step : Set := | P_LEFT : p_step -> p_step | P_RIGHT : p_step -> p_step | P_INVERT : step -> p_step - | P_STEP : step -> p_step - | P_NOP : p_step. + | P_STEP : step -> p_step. (* 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 @@ -2806,7 +2805,6 @@ Fixpoint p_rewrite (s : p_step) : proposition -> proposition := | P_RIGHT s => p_apply_right (p_rewrite s) | P_STEP s => move_right s | P_INVERT s => p_invert (move_right s) - | P_NOP => fun p : proposition => p end. Theorem p_rewrite_stable : forall s : p_step, prop_stable (p_rewrite s). @@ -2816,7 +2814,6 @@ Proof. - intros; apply p_apply_right_stable; trivial. - intros; apply p_invert_stable; apply move_right_stable. - apply move_right_stable. - - unfold prop_stable; simpl; intros; split; auto. Qed. Fixpoint normalize_hyps (l : list h_step) (lh : hyps) {struct l} : hyps := |