add EGlobal/RGlobal for CoreVars whose binder we cannot see

[coq-hetmet.git] / src / HaskStrongToProof.v

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 1efc666..143be0b 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -69,6 +69,7 @@ Context {VV:Type}{eqd_vv:EqDecidable VV}.
 
 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
   match exp as E in Expr Γ Δ ξ τ with
+  | EGlobal  Γ Δ ξ _ _                            => []
   | EVar     Γ Δ ξ ev                             => [ev]
   | ELit     Γ Δ ξ lit lev                        => []
   | EApp     Γ Δ ξ t1 t2 lev e1 e2                => (expr2antecedent e1),,(expr2antecedent e2)
@@ -585,6 +586,7 @@ Definition expr2proof  :
   refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
     : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
     match exp as E in Expr Γ Δ ξ τ with
+    | EGlobal  Γ Δ ξ t wev                          => let case_EGlobal := tt in _
     | EVar     Γ Δ ξ ev                             => let case_EVar := tt in _
     | ELit     Γ Δ ξ lit lev                        => let case_ELit := tt in _
     | EApp     Γ Δ ξ t1 t2 lev e1 e2                => let case_EApp := tt in 
@@ -630,6 +632,12 @@ Definition expr2proof  :
     end
 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
 
+    destruct case_EGlobal.
+      apply nd_rule.
+      simpl.
+      destruct t as [t lev].
+      apply (RGlobal _ _ _ _ wev).
+
     destruct case_EVar.
       apply nd_rule.
       unfold mapOptionTree; simpl.
@@ -704,6 +712,7 @@ Definition expr2proof  :
       auto.
 
     destruct case_ENote.
+      destruct t.
       eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
       apply e'.
       auto.