]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/decidable_kit/eqtype.ma
Most of the time, URIs can now be replaced with identifiers in "interpretation".
[helm.git] / helm / software / matita / library / decidable_kit / eqtype.ma
index 35f404df35aee4414ec589e47801c4cecbeba5a7..4b248a97e13799b02387f6297f1d5c06483af710 100644 (file)
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/decidable_kit/eqtype/".
-
 include "decidable_kit/decidable.ma".
 include "datatypes/constructors.ma".