[coq] start working on the coq impl, but stop

code/gcbpv.v

@@ -13,20 +13,17 @@ Record StCtx X := mkStCtx {
                       ty : StoupSem S -> X
                     }.
 
-Definition cdot X : StCtx X := mkStCtx _ None (fun x => match x with end).
-Definition hstoup Y (B : Y) : StCtx Y := mkStCtx _ One (fun x => match x with tt => B end).
+Definition cdot {X} : StCtx X := mkStCtx _ None (fun x => match x with end).
+Definition hstoup {Y} (B : Y) : StCtx Y := mkStCtx _ One (fun x => match x with tt => B end).
 
-Inductive Dimension := Top | Bot.
-Definition DCtx := StCtx Dimension.
-
-Inductive VType : DCtx -> Set :=
-  VUnit : forall I, VType I
-| VTimes : forall {I} (A A' : VType I), VType I
-| VU : forall {I} (B : CType I), VType I
+Inductive VType : Set :=
+  VUnit : VType
+| VTimes : forall (A A' : VType), VType
+| VU : forall (B : CType), VType
 with
-CType : DCtx -> Set :=
-| CTo : forall {I} (A : VType I) (B : CType I), CType I
-| CF  : forall {I} (A : VType I), CType I.
+CType : Set :=
+| CTo : forall (A : VType) (B : CType), CType
+| CF  : forall (A : VType), CType.
 
 Inductive Vlt : VType -> VType -> Set :=
   vrefl : forall A, Vlt A A
@@ -67,6 +64,8 @@ Definition ext (G : VCtx) (A : VType) : VCtx :=
               | inr tt => A            
             end).
 
+Definition CCtx := StCtx CType.
+
 Inductive Value : VCtx -> VType -> Type :=
 | var : forall G (x : U G), Value G (vty G x)
 | vunit : forall G, Value G VUnit
@@ -101,8 +100,3 @@ Term : VCtx -> CCtx -> CType -> Type :=
            Term G Dt B
 .
 
-
-
-
-asdf
-  . 
\ No newline at end of file