# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1227031749 18000
# Node ID 32ce9b28d7e78f72c8c1a0cc4393efd0bd2a7e1b
# Parent  cf5ddf078858177e151f49d62f68f814d8e5f361
Templatize Impure

diff -r cf5ddf078858 -r 32ce9b28d7e7 src/Impure.v
--- a/src/Impure.v	Tue Nov 18 13:04:39 2008 -0500
+++ b/src/Impure.v	Tue Nov 18 13:09:09 2008 -0500
@@ -67,6 +67,7 @@
     -> eval (c2 v1) v2
     -> eval (Bind c1 c2) v2.
 
+(* begin thide *)
   Fixpoint termDenote (e : term dynamic) : computation dynamic :=
     match e with
       | Var v => Return v
@@ -78,6 +79,7 @@
 
       | Unit => Return (Dyn tt)
     end.
+(* end thide *)
 
   Definition TermDenote (E : Term) := termDenote (E _).
 
@@ -87,15 +89,18 @@
   Eval compute in TermDenote ident_unit.
 
   Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt).
+(* begin thide *)
     compute.
     repeat econstructor.
     simpl.
     constructor.
   Qed.
+(* end thide *)
 
   Theorem invert_ident : forall (E : Term) d,
     eval (TermDenote (fun _ => ident _ @ E _)) d
     -> eval (TermDenote E) d.
+(* begin thide *)
     inversion 1.
 
     crush.
@@ -106,6 +111,7 @@
     simpl in H0.
     (** [injection H0.] *)
   Abort.
+(* end thide *)
 
 End impredicative.
 
@@ -147,6 +153,7 @@
     -> eval ds (f d2) ds' d3
     -> eval ds (CApp (Func i) d2) ds' d3.
 
+(* begin thide *)
   Fixpoint termDenote (e : term val) : computation :=
     match e with
       | Var v => Return v
@@ -157,6 +164,7 @@
 
       | Unit => Return VUnit
     end.
+(* end thide *)
 
   Definition TermDenote (E : Term) := termDenote (E _).
 
@@ -166,6 +174,7 @@
   Eval compute in TermDenote ident_unit.
 
   Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
+(* begin thide *)
     compute.
     repeat econstructor.
     simpl.
@@ -207,10 +216,12 @@
         | [ |- context[if ?E then _ else _] ] => destruct E
       end; crush.
   Qed.
+(* end thide *)
 
   Theorem invert_ident : forall (E : Term) ds ds' d,
     eval ds (TermDenote (fun _ => ident _ @ E _)) ds' d
     -> eval ((fun x => Return x) :: ds) (TermDenote E) ds' d.
+(* begin thide *)
     inversion 1; subst.
     clear H.
     inversion H3; clear H3; subst.
@@ -222,5 +233,6 @@
     inversion H7; clear H7; subst.
     assumption.
   Qed.
+(* end thide *)
 
 End predicative.