X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fteq_ext.ma;h=c71e77ddc08092f6821addff8855305a9fb15dcc;hp=c91f93e93a2cfcbc70b285bd722c22fe42feca9a;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma
index c91f93e93..c71e77ddc 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/teq_ext.ma
@@ -19,10 +19,10 @@ include "static_2/syntax/teq.ma".
 (* SYNTACTIC EQUIVALENCE ****************************************************)
 
 definition ceq: relation3 lenv term term ≝
-           ceqg (eq …).
+           ceqg (pr_eq …).
 
 definition ceq_ext: lenv → relation bind ≝
-           ceqg_ext (eq …).
+           ceqg_ext (pr_eq …).
 
 interpretation
   "context-dependent syntactic equivalence (term)"