# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1226344646 18000
# Node ID de33d1ed7c63036ff4ccaf640239bec4e59a83fc
# Parent  8f3fc56b90d496f1fe87699d3bbafae7809a014f
Templatize Extensional

diff -r 8f3fc56b90d4 -r de33d1ed7c63 src/Extensional.v
--- a/src/Extensional.v	Mon Nov 10 14:12:22 2008 -0500
+++ b/src/Extensional.v	Mon Nov 10 14:17:26 2008 -0500
@@ -103,6 +103,7 @@
 
     Definition ExpDenote t (e : Exp t) := expDenote (e _).
 
+(* begin thide *)
     Section exp_equiv.
       Variables var1 var2 : type -> Type.
 
@@ -129,6 +130,7 @@
 
     Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
       exp_equiv nil (E var1) (E var2).
+(* end thide *)
   End Source.
 
   Module CPS.
@@ -257,6 +259,7 @@
 
   Import Source CPS.
 
+(* begin thide *)
   Fixpoint cpsType (t : Source.type) : CPS.type :=
     match t with
       | Nat => Nat%cps
@@ -310,6 +313,7 @@
   Implicit Arguments cpsExp [var t].
   Definition CpsExp (E : Exp Nat) : Prog :=
     fun var => cpsExp (E _) (PHalt (var := _)).
+(* end thide *)
 
   Eval compute in CpsExp zero.
   Eval compute in CpsExp one.
@@ -323,6 +327,7 @@
   Eval compute in ProgDenote (CpsExp app_ident).
   Eval compute in ProgDenote (CpsExp app_ident').
 
+(* begin thide *)
   Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
     match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with
       | Nat => fun n1 n2 => n1 = n2
@@ -373,6 +378,7 @@
       generalize (cpsExp_correct (e1 := E _) (e2 := E _)
         (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
   Qed.
+(* end thide *)
 
 End STLC.