1. bug in addition of universe constraints fixed: the recursive

[helm.git] / matita / components / ng_kernel / nCicEnvironment.mli

diff --git a/matita/components/ng_kernel/nCicEnvironment.mli b/matita/components/ng_kernel/nCicEnvironment.mli
index 5128831bea9ed279a6097203e99e253578294e6c..8483b8a1f771c17be9651dbf83458064051b5115 100644 (file)
--- a/matita/components/ng_kernel/nCicEnvironment.mli
+++ b/matita/components/ng_kernel/nCicEnvironment.mli
@@ -37,7 +37,6 @@ val get_checked_fixes_or_cofixes:
   NReference.reference -> 
    NCic.inductiveFun list * NCic.f_attr * int
 
-(* invalidate the object and all those that entered the environment after it *)
 val invalidate_item: 
       [ `Obj of NUri.uri * NCic.obj 
       | `Constr of NCic.universe * NCic.universe ] -> unit