X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fgdrop.ma;h=ba2be29cc499f7d1aa5d134dde5385e7f0357afc;hb=cdfd45ca5a2b52601b7bde732a7811de55a52fed;hp=218389e1ce7fd2a322d1b0835bd20d6b4aa017ac;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma
index 218389e1c..ba2be29cc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma
@@ -22,7 +22,7 @@ inductive gdrop (e:nat): relation genv ≝
 | gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. ⓑ{I} V) G2
 .
 
-interpretation "global slicing" 
+interpretation "global slicing"
    'RDrop e G1 G2 = (gdrop e G1 G2).
 
 (* basic inversion lemmas ***************************************************)