From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 15 Nov 2008 15:20:33 +0000 (+0000)
Subject: fixed not-e
X-Git-Tag: make_still_working~4553
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbce2f96c977d51ac2843e98a224aa4dae7ea3b2;p=helm.git

fixed not-e
---

diff --git a/helm/software/matita/library/didactic/support/natural_deduction.ma b/helm/software/matita/library/didactic/support/natural_deduction.ma
index 3e7c54d5c..b7ee07cb6 100644
--- a/helm/software/matita/library/didactic/support/natural_deduction.ma
+++ b/helm/software/matita/library/didactic/support/natural_deduction.ma
@@ -450,7 +450,7 @@ interpretation "Not_elim_ok_2" 'Not_elim_ok_2 ab a b =
 notation > "¬_'e' term 90 ab term 90 a" with precedence 19
 for @{ 'Not_elim (show $ab ?) (show $a ?) }.
 interpretation "Not_elim KO" 'Not_elim ab a = 
-  (cast _ _ (Not_elim _ (cast _ _ ab) (cast _ _ a))).
+  (cast _ _ (Not_elim unit (cast _ _ ab) (cast _ _ a))).
 interpretation "Not_elim OK" 'Not_elim ab a = 
   (Not_elim _ ab a).