update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / syntax / label.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
index 1241db40aaa5bcdf36dc27d461ce6f29ac6e40c5..bdeaa9c20102004b337e6d4e264baa51ade8da92 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/label.ma
@@ -27,8 +27,6 @@ inductive label: Type[0] ≝
 | label_edge_s: label
 .
 
-coercion label_node_d.
-
 interpretation
   "variable reference by depth (label)"
   'NodeLabelD p = (label_node_d p).