X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofCategory.v;h=18da307b34816ce21eafa61ef2ca1a54aea9f9e1;hp=e74d5808cc81f72f73060312831b6d9399a7ad92;hb=fd337b235014f43000773eb0d95168d89e93a893;hpb=50747fb9b9a44a24ea7a29b8703706386f6cd092

diff --git a/src/HaskProofCategory.v b/src/HaskProofCategory.v
index e74d580..18da307 100644
--- a/src/HaskProofCategory.v
+++ b/src/HaskProofCategory.v
@@ -44,15 +44,13 @@ Open Scope nd_scope.
 
 Section HaskProofCategory.
 
-  Implicit Arguments RURule [[Γ][Δ][h][c]].
-
   Context (ndr_systemfc:@ND_Relation _ Rule).
 
   (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows     *)
   (* Rule_PCF consists of the rules allowed in flat PCF: everything except *)
   (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements        *)
   Inductive Rule_PCF {Γ}{Δ} : ∀ h c, Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) -> Type :=
-  | PCF_RCanL            : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a              ))
+  | PCF_RArrange         : ∀ x y              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a              ))
   | PCF_RCanR            : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanR t a              ))
   | PCF_RuCanL           : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanL t a             ))
   | PCF_RuCanR           : ∀ t a              ,  Rule_PCF  [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanR t a             ))