X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=354e559b30248d7d81c045a916b21b97bd9350da;hp=64746651808aab81c04759c3602f3f845936b742;hb=ff9fafbf161b4f12688d5986518be874d39ab3ee;hpb=693c6f552555f14c085a71e0b03c67d3c051eaa1

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 6474665..354e559 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -16,6 +16,7 @@ Require Import HaskKinds.
 Require Import HaskCoreTypes.
 Require Import HaskLiteralsAndTyCons.
 Require Import HaskStrongTypes.
+Require Import HaskWeakVars.
 
 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
  * in any context of that shape.  Notice that the succedent contains a tree of types rather than a single type; think
@@ -90,6 +91,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
 
 (* SystemFC rules *)
 | RVar    : ∀ Γ Δ σ       l,                          Rule [                                 ]   [Γ>Δ> [σ@@l]   |- [σ          @@l]]
+| RGlobal : ∀ Γ Δ τ       l,   WeakExprVar ->         Rule [                                 ]   [Γ>Δ>     []   |- [τ          @@l]]
 | RLam    : forall Γ Δ Σ (tx:HaskType Γ ★) te l,      Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l]        ]   [Γ>Δ>    Σ     |- [tx--->te   @@l]]
 | RCast   : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
 HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->