X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=0d33b0aebfe6986efb3c9a0bc4b0ef8eaad5f4e5;hp=bdcf1e65cbd882ad46aaa6891205bee60ed07666;hb=a4a1bd8f36776aa8dd9393cf8d2b6afa0172e978;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index bdcf1e6..0d33b0a 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -101,7 +101,7 @@ Fixpoint typeToLatexMath (needparens:bool){κ}(t:RawHaskType (fun _ => LatexMath
                                       ; let body := t1'+++(rawLatexMath " ")+++t2'
                                         in return (if needparens then (rawLatexMath "(")+++body+++(rawLatexMath ")") else body)
                 end
-  | TyFunApp   tfc lt  => bind rest = typeListToRawLatexMath false lt
+  | TyFunApp   tfc _ _ lt  => bind rest = typeListToRawLatexMath false lt
                         ; return (rawLatexMath "{\text{\tt{")+++(toLatexMath (toString tfc))+++(rawLatexMath "}}}")+++
                                  (rawLatexMath "_{")+++(rawLatexMath (toString (length (fst (tyFunKind tfc)))))+++
                                  (rawLatexMath "}")+++
@@ -126,7 +126,7 @@ Definition ltypeToLatexMath {Γ:TypeEnv}{κ}(t:LeveledHaskType Γ κ) : VarNameS
     | nil => t''
     | lv  => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
            (fold_left (fun x y => x+++(rawLatexMath ":")+++y)
-             (map (fun l:HaskTyVar Γ ★ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
+             (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
     end
     end); try apply ConcatenableLatexMath.
     try apply VarNameMonad.
@@ -187,12 +187,12 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
     | RAbsCo        _ _ _ _ _ _ _ _   => "AbsCo"
     | RApp          _ _ _ _ _ _ _     => "App"
     | RLet          _ _ _ _ _ _ _     => "Let"
-    | RBindingGroup _ _ _ _ _ _       => "RBindingGroup"
+    | RJoin _ _ _ _ _ _       => "RJoin"
     | RLetRec       _ _ _ _ _ _       => "LetRec"
     | RCase         _ _ _ _ _ _ _ _   => "Case"
     | RBrak         _ _ _ _ _ _       => "Brak"
     | REsc          _ _ _ _ _ _       => "Esc"
-    | REmptyGroup   _ _               => "REmptyGroup"
+    | RVoid   _ _               => "RVoid"
 end.
 
 Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
@@ -215,8 +215,8 @@ Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
 Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
   match r with
     | RArrange      _ _ _ _ _ r => nd_hideURule r
-    | REmptyGroup   _ _         => true
-    | RBindingGroup _ _ _ _ _ _ => true
+    | RVoid   _ _         => true
+    | RJoin _ _ _ _ _ _ => true
     | _                         => false
   end.
 
@@ -224,5 +224,5 @@ Instance ToLatexMathRule h c : ToLatexMath (Rule h c) :=
   { toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
 
 Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
-@SCND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
-  (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
+@SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
+  (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).