Universes introduction

[helm.git] / helm / ocaml / cic_transformations / acic2Ast.ml

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index e51e9c0a401b3d69accb7790a364e6243ab12836..1bc76ebb841176b185fde2c0052e2168b7130d0a 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -78,7 +78,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, astcontext_of_ciccontext l))
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
-    | Cic.ASort (id,Cic.Type) -> idref id (Ast.Sort `Type)
+    | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) (* TASSI *)
     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
     | Cic.AImplicit _ -> assert false
     | Cic.AProd (id,n,s,t) ->