diff options
Diffstat (limited to 'contrib/xml/cic2acic.ml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 6ea000f5b..1a6cb9c81 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 = |