]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/cicUniv.mli
CicUniv.UniverseInconsistency is no handled correcly.
[helm.git] / helm / software / components / cic / cicUniv.mli
index eb3c50866f73482a578f0f8376bd376c8e124236..288efe616885b833ceedb5984af376fda2f8b2ae 100644 (file)
@@ -27,7 +27,7 @@
 (*
   The strings contains an unreadable message
 *)
-exception UniverseInconsistency of string
+exception UniverseInconsistency of string Lazy.t
 
 (*
   Cic.Type of universe 
@@ -136,7 +136,7 @@ val recons_graph: universe_graph -> universe_graph
   (** re-hash-cons a single universe *)
 val recons_univ: universe -> universe
 
-  (** consistency chek that should be done before committin the graph to the
+  (** consistency check that should be done before committin the graph to the
    * cache *)
 val assert_univs_have_uri: universe_graph -> universe list-> unit