From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jun 2011 10:22:29 +0000 (+0000)
Subject: Remove the daemon :-)
X-Git-Tag: make_still_working~2431
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0e81e658803822599b5e015aab67bc282afc9c4d;p=helm.git

Remove the daemon :-)
---

diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma
index ad3aa9371..9f2d758c1 100644
--- a/matita/matita/lib/basics/jmeq.ma
+++ b/matita/matita/lib/basics/jmeq.ma
@@ -51,8 +51,6 @@ lemma gral: ∀A.∀x,y:A.
  #H @H
 qed.
 
-axiom daemon: False.
-
 lemma jm_to_eq_sigma:
  ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y.
  #A #x #y #E cases E in ⊢ (???%); %