3 problems solved patching the alpha-conversion of coq 7.3.1

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Level-1 / LambdaDelta / theory.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
index 405f95aff0dc033084bbee5f073d384de3d05945..8b96936ab016f1bea87eb25dc1e30c1b4a2d9ed2 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma
@@ -176,5 +176,7 @@ include "aplus/props.ma".
 
 include "leq/defs.ma".
 
+include "leq/props.ma".
+
 include "leq/asucc.ma".