X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLegacy-2%2Fpreamble.ma;h=00c38151d1826bb28550294d28b98cf11ca1c0b9;hb=e78cf74f8976cf0ca554f64baa9979d0423ee927;hp=0666938e899ecbd2702454f0995f6e0ecb8984f3;hpb=c6094ab9349aaa41a8c29c5773a3e756ac819e7f;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
index 0666938e8..00c38151d 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
@@ -39,7 +39,7 @@ interpretation "Coq 7.3.1 natural minus" 'minus x y = (cic:/matita/LAMBDA-TYPES/
 interpretation "Coq 7.3.1 logical and" 'and x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/land.ind#xpointer(1/1) x y).
 interpretation "Coq 7.3.1 logical or" 'or x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/or.ind#xpointer(1/1) x y).
 interpretation "Coq 7.3.1 logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/not.con x).
-interpretation "Coq 7.3.1 exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
+interpretation "Coq 7.3.1 exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) ? x).
 interpretation "Coq 7.3.1 natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
 interpretation "Coq 7.3.1 natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
 interpretation "Coq 7.3.1 leibnitz's equality" 'eq t x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) t x y).