partial update in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / teq_ext.ma

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 c71e77ddc08092f6821addff8855305a9fb15dcc..c91f93e93a2cfcbc70b285bd722c22fe42feca9a 100644 (file)
--- 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)"