ocaml 3.09 transition

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / ty0_props.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v
index d51266a540ffb7a2464e24e49987a3d28fcf4001..ab4b0068711eba23016af3ecbbdc1d402f09728a 100644 (file)
--- 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 *)