added universes

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index e9ce2e81ca002ea8572bf46a0e1209279a53a62a..d267b52b1ff39ab713b815914e5448bb799bb563 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -318,7 +318,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
         Cic.Meta (index, cic_subst)
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
-    | CicNotationPt.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
+    | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
     | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()