]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
contribs should now compile
[helm.git] / matita / contribs / LAMBDA-TYPES / Unified-Sub / Lift / defs.ma
index b8a4e2a85972574989bfc7f90922e3e0b11c0e43..fb71d39767073de0b032a3de013fd8de7ae27499 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
+
 
 (* LIFT RELATION
    - Usage: invoke with positive polarity