Dummy dependent products in inductive types arities are no longer cleaned.

[helm.git] / helm / software / matita / library / nat / relevant_equations.ma

diff --git a/helm/software/matita/library/nat/relevant_equations.ma b/helm/software/matita/library/nat/relevant_equations.ma
index 6e641708021d79d36c81b67283f889949e1fe43c..a2ef6e40cdc6ffaba378c058d3a030a6fa9bea9d 100644 (file)
--- a/helm/software/matita/library/nat/relevant_equations.ma
+++ b/helm/software/matita/library/nat/relevant_equations.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/relevant_equations".
-
 include "nat/times.ma".
 include "nat/minus.ma".
 include "nat/gcd.ma".