X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fty0_props.v;h=ab4b0068711eba23016af3ecbbdc1d402f09728a;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=d51266a540ffb7a2464e24e49987a3d28fcf4001;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v
index d51266a54..ab4b00687 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v
@@ -1,6 +1,7 @@
 Require drop_props.
 Require pc3_props.
 Require ty0_defs.
+Require ty0_gen.
 Require ty0_lift.
 
    Section ty0_correct. (****************************************************)
@@ -71,10 +72,12 @@ Require ty0_lift.
 
       Hints Resolve ty0_shift : ltlc.
 
-(*#* #start file *)
-
    Section ty0_unique. (*****************************************************)
 
+      Opaque pc3.
+
+(*#* #start file *)
+
 (*#* #caption "uniqueness of types" *)
 (*#* #cap #cap c, t1, t2 #alpha u in T *)