-%% test per matita.lang
+set "baseuri" "cic:/matita/tests/grafite/".
-set "baseuri" "cic:/matita/tests/".
-
-%% commento
(* commento *)
-(** hint. **)
+(** hint. *)
inductive pippo : Type \def
| a : Type \to pippo
whelp locate pippo.
print "coercions".
-
-
-