]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma
- some confluence results for focalized reduction and computation
[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / substitution / gdrop_gdrop.ma
index 640c36c7802ec97fab7f6c0074a34e1a4ffa98cc..0bc1a40d5dda09f8bb559c51b31d8b9ec0bdbe80 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/substitution/gdrop.ma".
+include "basic_2/substitution/gdrop.ma".
 
 (* GLOBAL ENVIRONMENT SLICING ***********************************************)