X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToLatex.v;h=e239205f2cbdac6727d6d024b3a2788753d64f22;hp=55496dc9411a478646f18565963d6b54d3c29d44;hb=061af1379740c1118e42ae7c37ea294b4c2174f3;hpb=703bff3b209bd7d114b49cb736da8af167a4ec71

diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v
index 55496dc..e239205 100644
--- a/src/HaskProofToLatex.v
+++ b/src/HaskProofToLatex.v
@@ -206,8 +206,6 @@ Section ToLatex.
     end.
 End ToLatex.
 
-Axiom systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
-
 Definition nd_ml_toLatex {c}(pf:@ND _ Rule [] c) :=
   @SCND_toLatex _ _
       judgment2latex