- improved Makefile esp. with the "trim" function

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / gdrop.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gdrop.ma
index 218389e1ce7fd2a322d1b0835bd20d6b4aa017ac..ba2be29cc499f7d1aa5d134dde5385e7f0357afc 100644 (file)
--- 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 ***************************************************)