X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprova.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprova.ma;h=a3357f8e0d62f977e059418a4cbad07f21384c44;hb=3ce05ecd50428a27ce17adb070620aeeaf2aed65;hp=7751a0d1f62476d90a4241d96f1c5d8c87a2fc1d;hpb=13c9f0ee2525769013a93333c4c8a65e603cc705;p=helm.git

diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index 7751a0d1f..a3357f8e0 100644
--- a/helm/software/matita/contribs/prova.ma
+++ b/helm/software/matita/contribs/prova.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/tests".
+set "baseuri" "cic:/matita/test/prova".
 
-include "../contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma".
+include "../contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma".
 
 alias id "Abbr" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/1)".
 alias id "Abst" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/B.ind#xpointer(1/1/2)".
@@ -51,3 +51,10 @@ alias id "THead" = "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs/T.ind#xp
 
 inline procedural
    "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props/pr0_subst0.con".
+(*
+inline procedural
+   "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3/ty3_sred_wcpr0_pr0.con".
+
+inline procedural
+   "cic:/Coq/Reals/RiemannInt/FTC_Riemann.con".
+*)