clean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files

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

diff --git a/src/HaskStrongToWeak.v b/src/HaskStrongToWeak.v
index 1761b83..79d954c 100644 (file)
--- a/src/HaskStrongToWeak.v
+++ b/src/HaskStrongToWeak.v
@@ -181,7 +181,7 @@ Section HaskStrongToWeak.
                                   (fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
                   ; return WECase vscrut' escrut' tbranches' tc tys branches'
 
-    | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
+    | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
                                                                         => bind tleaf = typeToWeakType (snd vt) ite
                                                                          ; bind v' = mkWeakExprVar tleaf
                                                                          ; return ((fst vt),v'))
@@ -213,4 +213,4 @@ Section HaskStrongToWeak.
       uniqM f => f us >>= fun x => OK (snd x)
       end.
 
-End HaskStrongToWeak.
\ No newline at end of file
+End HaskStrongToWeak.