X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=139a6417a3c33c6f6f4fb4328794ac4802a5195c;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=b09f0a8ef1bd340eb41e2d127f3b6aae8bed1964;hpb=c0e0ae45ee6fba4118f519b9d07169ed6a7edc8c;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index b09f0a8ef..139a6417a 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -257,7 +257,7 @@ let interpretate ~context ~env ast =
         Cic.Meta (index, cic_subst)
     | CicAst.Sort `Prop -> Cic.Sort Cic.Prop
     | CicAst.Sort `Set -> Cic.Sort Cic.Set
-    | CicAst.Sort `Type -> Cic.Sort Cic.Type
+    | CicAst.Sort `Type -> Cic.Sort (Cic.Type (CicUniv.fresh())) (* TASSI *)
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()