removed daemons

[helm.git] / matita / matita / contribs / lambda / paths / dst_computation.ma

diff --git a/matita/matita/contribs/lambda/paths/dst_computation.ma b/matita/matita/contribs/lambda/paths/dst_computation.ma
index 2e5310a1103d046d97a1b0f0919761b40f87d959..f7740daf7420fa470a0a8b4ff7c4f8629f710171 100644 (file)
--- a/matita/matita/contribs/lambda/paths/dst_computation.ma
+++ b/matita/matita/contribs/lambda/paths/dst_computation.ma
@@ -27,11 +27,11 @@ inductive dst: relation term ≝
 .
 
 interpretation "decomposed standard computation"
-    'Std M N = (dst M N).
+    'DecomposedStd M N = (dst M N).
 
 notation "hvbox( M break ⓢ↦* term 46 N )"
    non associative with precedence 45
-   for @{ 'Std $M $N }.
+   for @{ 'DecomposedStd $M $N }.
 
 lemma dst_inv_lref: ∀M,N. M ⓢ↦* N → ∀j. #j = N →
                     ∃∃s. is_whd s & M ↦*[s] #j.