]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_1/G/defs.ma
update in basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / G / defs.ma
index 23edf578984153bcc9c9068c4c7baf9b08041dcd..ae81c7857dd23e5cea3ae2b977fa51f4192fbef4 100644 (file)
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/preamble.ma".
+include "basic_1/preamble.ma".
 
-record G : Set \def {
+record G : Type[0] \def {
  next: (nat \to nat);
  next_lt: (\forall (n: nat).(lt n (next n)))
 }.