From: Claudio Sacerdoti Coen Date: Mon, 26 Sep 2005 16:25:07 +0000 (+0000) Subject: Coq's existential fixed. X-Git-Tag: V_0_7_2_3~311 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4628e72aa23c1f077f483c62f373784f9f3c3aad;p=helm.git Coq's existential fixed. --- diff --git a/helm/matita/coq.ma b/helm/matita/coq.ma index 4c3d8f772..10a3de677 100644 --- a/helm/matita/coq.ma +++ b/helm/matita/coq.ma @@ -24,7 +24,7 @@ interpretation "Coq's binary integer unary minus" 'uminus x = (cic:/Coq/ZArith/B interpretation "Coq's logical and" 'and x y = (cic:/Coq/Init/Logic/and.ind#xpointer(1/1) x y). interpretation "Coq's logical or" 'or x y = (cic:/Coq/Init/Logic/or.ind#xpointer(1/1) x y). interpretation "Coq's logical not" 'not x = (cic:/Coq/Init/Logic/not.con x). -interpretation "Coq's exists" 'exists x y = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) x y). +interpretation "Coq's exists" 'exists \eta.x = (cic:/Coq/Init/Logic/ex.ind#xpointer(1/1) _ x). (* relational operators *)