]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/tests/bad_induction.ma
End of patch for computation of LetIn types. Now types of mutually (co)recursive
[helm.git] / helm / software / matita / tests / bad_induction.ma
index b009e18d15d04aea4302428a440804967931a580..172aa8e117a87efc75d3c7a8ab3be7348d701ec2 100644 (file)
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/bad_induction".
+
 
 include "nat/nat.ma".