nasty change in the lexer/parser:

[helm.git] / helm / software / matita / contribs / dama / dama_duality / constructive_connectives.ma

diff --git a/helm/software/matita/contribs/dama/dama_duality/constructive_connectives.ma b/helm/software/matita/contribs/dama/dama_duality/constructive_connectives.ma
index 4d2ea5996df11e814f6a5847385f9fc0ed2da4fe..3c866b2ad8e2171aec1bcfa8e3aee85dff205483 100644 (file)
--- a/helm/software/matita/contribs/dama/dama_duality/constructive_connectives.ma
+++ b/helm/software/matita/contribs/dama/dama_duality/constructive_connectives.ma
@@ -39,8 +39,8 @@ for @{ 'sigma ${default
   @{\lambda ${ident i} . $p}}}.
 *)
 
-interpretation "constructive exists" 'exists \eta.x = (ex _ x).
-interpretation "constructive exists (Type)" 'exists \eta.x = (exT _ x).
+interpretation "constructive exists" 'exists \eta.x = (ex ? x).
+interpretation "constructive exists (Type)" 'exists \eta.x = (exT ? x).
 
 alias id "False" = "cic:/matita/logic/connectives/False.ind#xpointer(1/1)".
 definition Not ≝ λx:Type.x → False.