diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/pcicenv.ml | 2 | ||||
| -rw-r--r-- | contrib/xml/cic2acic.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml index c9c0ed4b21..4ac4e9704e 100644 --- a/contrib/correctness/pcicenv.ml +++ b/contrib/correctness/pcicenv.ml @@ -38,7 +38,7 @@ let add_sign (id,t) s = let cast_set c = mkCast (c, mkSet) -let set = mkCast (mkSet, mkType Univ.prop_univ) +let set = mkCast (mkSet, mkType Univ.type1_univ) (* [cci_sign_of env] construit un environnement pour CIC ne comprenant que * les objets fonctionnels de l'environnement de programes [env] diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 6ea000f5b6..1a6cb9c811 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -263,7 +263,7 @@ let typeur sigma metamap = match sort_of env cstr with Coq_sort T.InProp -> T.mkProp | Coq_sort T.InSet -> T.mkSet - | Coq_sort T.InType -> T.mkType Univ.prop_univ (* ERROR HERE *) + | Coq_sort T.InType -> T.mkType Univ.type1_univ (* ERROR HERE *) | CProp -> T.mkConst DoubleTypeInference.cprop and sort_of env t = |