]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicEnvironment.mli
positivity check fixed
[helm.git] / helm / software / components / ng_kernel / nCicEnvironment.mli
index 67b3857d1703f71ea1cb0abe191247fc3c974090..029cd94d18818a0c3520f0ce0f2360f6829b56ae 100644 (file)
@@ -29,6 +29,7 @@ val universe_leq: NCic.universe -> NCic.universe -> bool
    true -> strict check (<); false -> loose check (<=)
 *)
 val add_constraint: bool -> NCic.universe -> NCic.universe -> unit
+val pp_constraints: unit -> string
 
 val get_checked_def:
   NReference.reference ->