simpl -> cbn

1 files changed, 20 insertions, 20 deletions

diff --git a/kvx/Asm.v b/kvx/Asm.v
index 30aafc55..515e13e0 100644
--- a/kvx/Asm.v
+++ b/kvx/Asm.v
@@ -611,15 +611,15 @@ Program Definition genv_trans (ge: genv) : Asmvliw.genv :=
       Genv.genv_defs := PTree.map1 globdef_proj (Genv.genv_defs ge);
       Genv.genv_next := Genv.genv_next ge |}.
 Next Obligation.
-  destruct ge. simpl in *. eauto.
+  destruct ge. cbn in *. eauto.
 Qed. Next Obligation.
-  destruct ge; simpl in *.
+  destruct ge; cbn in *.
   rewrite PTree.gmap1 in H.
   destruct (genv_defs ! b) eqn:GEN.
   - eauto.
   - discriminate.
 Qed. Next Obligation.
-  destruct ge; simpl in *.
+  destruct ge; cbn in *.
   eauto.
 Qed.
 
@@ -655,14 +655,14 @@ Program Definition transf_function (f: Asmvliw.function) : function :=
 
 Lemma transf_function_proj: forall f, function_proj (transf_function f) = f.
 Proof.
-  intros f. destruct f as [sig blks]. unfold function_proj. simpl. auto.
+  intros f. destruct f as [sig blks]. unfold function_proj. cbn. auto.
 Qed.
 
 Definition transf_fundef : Asmvliw.fundef -> fundef := AST.transf_fundef transf_function.
 
 Lemma transf_fundef_proj: forall f, fundef_proj (transf_fundef f) = f.
 Proof.
-  intros f. destruct f as [f|e]; simpl; auto.
+  intros f. destruct f as [f|e]; cbn; auto.
   rewrite transf_function_proj. auto.
 Qed.
 
@@ -674,18 +674,18 @@ Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),
   prog_main p1 = prog_main p2 ->
   p1 = p2.
 Proof.
-  intros. destruct p1. destruct p2. simpl in *. subst. auto.
+  intros. destruct p1. destruct p2. cbn in *. subst. auto.
 Qed.
 
 Lemma transf_program_proj: forall p, program_proj (transf_program p) = p.
 Proof.
-  intros p. destruct p as [defs pub main]. unfold program_proj. simpl.
-  apply program_equals; simpl; auto.
+  intros p. destruct p as [defs pub main]. unfold program_proj. cbn.
+  apply program_equals; cbn; auto.
   induction defs.
-  - simpl; auto.
-  - simpl. rewrite IHdefs. 
-    destruct a as [id gd]; simpl.
-    destruct gd as [f|v]; simpl; auto.
+  - cbn; auto.
+  - cbn. rewrite IHdefs. 
+    destruct a as [id gd]; cbn.
+    destruct gd as [f|v]; cbn; auto.
     rewrite transf_fundef_proj. auto.
 Qed.
 
@@ -707,16 +707,16 @@ Lemma match_program_transf:
   forall p tp, match_prog p tp -> transf_program p = tp.
 Proof.
   intros p tp H. inversion_clear H. inv H1.
-  destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *.
-  subst. unfold transf_program. unfold transform_program. simpl.
-  apply program_equals; simpl; auto.
-  induction H0; simpl; auto.
+  destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. cbn in *.
+  subst. unfold transf_program. unfold transform_program. cbn.
+  apply program_equals; cbn; auto.
+  induction H0; cbn; auto.
   rewrite IHlist_forall2. apply cons_extract.
   destruct a1 as [ida gda]. destruct b1 as [idb gdb].
-  simpl in *.
+  cbn in *.
   inv H. inv H2.
-  - simpl in *. subst. auto.
-  - simpl in *. subst. inv H. auto.
+  - cbn in *. subst. auto.
+  - cbn in *. subst. inv H. auto.
 Qed.
 
 Section PRESERVATION.
@@ -744,7 +744,7 @@ Proof.
   pose proof (match_program_transf prog tprog TRANSF) as TR.
   subst. unfold semantics. rewrite transf_program_proj.
 
-  eapply forward_simulation_step with (match_states := match_states); simpl; auto.
+  eapply forward_simulation_step with (match_states := match_states); cbn; auto.
   - intros. exists s1. split; auto. congruence.
   - intros. inv H. auto.
   - intros. exists s1'. inv H0. split; auto. congruence.