X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcoq.ma;h=1b284799dfefbec04e98d52f1d5ef72ab73fffb9;hb=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;hp=4c3d8f772780e6e8cc011743ea55cf4905fd5b13;hpb=56062350e31144f05421de6f895101ab3defc324;p=helm.git

diff --git a/helm/matita/coq.ma b/helm/matita/coq.ma
index 4c3d8f772..1b284799d 100644
--- a/helm/matita/coq.ma
+++ b/helm/matita/coq.ma
@@ -1,3 +1,5 @@
+set "baseuri" "cic:/Coq/".
+
 (* aritmetic operators *)
 
 interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
@@ -24,7 +26,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 *)