X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=e4281d7b7ece02bfe3f93544beb6ee1d0efdb907;hp=3cd8ff6b5c577bbdd8da0626679627018f2411c6;hb=164cdbf41ca206079b0dcfc18cd13625b286c38c;hpb=d684a61025d30f0ae06893298f126ae0072d6922

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 3cd8ff6..e4281d7 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -236,12 +236,13 @@ Section core2proof.
     ND Rule 
        [ Γ > Δ > Σ             |- [a ---> s @@ lev ] ]
        [ Γ > Δ > Σ,,[a @@ lev] |-       [ s @@ lev ] ].
-    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ Σ [a@@lev] a s lev) ].
-    eapply nd_comp; [ apply nd_rlecnac | idtac ].
-    apply nd_prod.    
-    apply nd_id.
+    eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; apply RExch ].
+    eapply nd_comp; [ idtac | eapply nd_rule; apply (@RApp Γ Δ [a@@lev] Σ a s lev) ].
+    eapply nd_comp; [ apply nd_llecnac | idtac ].
+    apply nd_prod.
     apply nd_rule.
     apply RVar.
+    apply nd_id.
     Defined.
 
   Definition fToC1 {Γ}{Δ}{a}{s}{lev} :