X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FHaskProof.v;h=ef669eee0abc1dd87000d2035893700e283c9e15;hb=fa3f21c9f6460d761f3b33f00e4414ad2710099d;hp=55b0b032a6f5655002f2729462d42122aeaf96ab;hpb=b3214686b18b2d6f6905394494da8d1c17587bdb;p=coq-hetmet.git

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 55b0b03..ef669ee 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -133,7 +133,8 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
 | Flat_RApp             : ∀ Γ Δ  Σ tx te   p     l,  Rule_Flat (RApp Γ Δ  Σ tx te   p l)
 | Flat_RLet             : ∀ Γ Δ  Σ σ₁ σ₂   p     l,  Rule_Flat (RLet Γ Δ  Σ σ₁ σ₂   p l)
 | Flat_RBindingGroup    : ∀ q a b c d e ,  Rule_Flat (RBindingGroup q a b c d e)
-| Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x).
+| Flat_RCase            : ∀ Σ Γ  T κlen κ θ l x  , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
+| Flat_RLetRec          : ∀ Γ Δ Σ₁ τ₁ τ₂ lev,      Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
 
 (* given a proof that uses only uniform rules, we can produce a general proof *)
 Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)