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=c91f93e93a2cfcbc70b285bd722c22fe42feca9a;hp=c71e77ddc08092f6821addff8855305a9fb15dcc;hb=156d974ad89aa04a086fdf9d332c8b04adf279fd;hpb=8fe4dc148d50a0352313633bea61441bc817afbf

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 c71e77ddc..c91f93e93 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 (pr_eq …).
+           ceqg (eq …).
 
 definition ceq_ext: lenv → relation bind ≝
-           ceqg_ext (pr_eq …).
+           ceqg_ext (eq …).
 
 interpretation
   "context-dependent syntactic equivalence (term)"