- lambda_delta: morew propertie in context-sensitive computation

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / item.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
index 89f1a94e4d2eef0997f041f93bf099c4539d6920..7e4ee38398b7d8d229597ad75b1ce79cfb50c9a8 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
@@ -42,9 +42,9 @@ inductive item2: Type[0] ≝
   | Flat2: flat2 → item2 (* non-binding item *)
 .
 
-coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind2 on _I:bind2 to item2.
+coercion Bind2.
 
-coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat2 on _I:flat2 to item2.
+coercion Flat2.
 
 (* Basic properties *********************************************************)