X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=2508976c35b52cbad2fb7dc7946657dc3d93c6a4;hp=606b667723acb7cada6a7c63f2ee10d248ac29f5;hb=8282f5a7639dbe862bba29d3170d58b81bbb1446;hpb=02af384ece10c5aa927c7d7c1379e9d202926cc8

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 606b667..2508976 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -49,12 +49,13 @@ Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
 
 (* information needed to define a case branch in a HaskProof *)
 Record ProofCaseBranch {n}{tc:TyCon n}{Γ}{lev}{branchtype : HaskType Γ}{avars} :=
-{ cbi_cbi              :  @StrongAltConInContext n tc Γ avars
-; cbri_freevars        :  Tree ??(LeveledHaskType Γ)
-; cbri_judg            := cbi_Γ cbi_cbi > cbi_Δ  cbi_cbi
-                          > (mapOptionTree weakLT' cbri_freevars),,(unleaves (vec2list (cbi_types cbi_cbi)))
+{ pcb_scb            :  @StrongCaseBranch n tc Γ avars
+; pcb_freevars        :  Tree ??(LeveledHaskType Γ)
+; pcb_judg            := scb_Γ pcb_scb > scb_Δ  pcb_scb
+                          > (mapOptionTree weakLT' pcb_freevars),,(unleaves (vec2list (scb_types pcb_scb)))
                           |- [weakLT' (branchtype @@ lev)]
 }.
+Coercion pcb_scb : ProofCaseBranch >-> StrongCaseBranch.
 Implicit Arguments ProofCaseBranch [ ].
 
 (* Figure 3, production $\vdash_E$, Uniform rules *)
@@ -108,9 +109,9 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 | RCase          : forall Γ Δ lev n tc Σ avars tbranches
   (alts:Tree ??(@ProofCaseBranch n tc Γ lev tbranches avars)),
                    Rule
-                       ((mapOptionTree cbri_judg alts),,
+                       ((mapOptionTree pcb_judg alts),,
                         [Γ > Δ >                                               Σ |- [ caseType tc avars @@ lev ] ])
-                        [Γ > Δ > (mapOptionTreeAndFlatten cbri_freevars alts),,Σ |- [ tbranches         @@ lev ] ]
+                        [Γ > Δ > (mapOptionTreeAndFlatten pcb_freevars alts),,Σ |- [ tbranches         @@ lev ] ]
 .
 Coercion RURule : URule >-> Rule.