last comment was incomplete by mistake.

[helm.git] / matita / components / ng_kernel / nCic.ml

diff --git a/matita/components/ng_kernel/nCic.ml b/matita/components/ng_kernel/nCic.ml
index 03672a0c46c2d9c446fb4a6b5075b6c226b239d0..ebf6f8ef5139779ecc517e0fb9ee83568c14880e 100644 (file)
--- a/matita/components/ng_kernel/nCic.ml
+++ b/matita/components/ng_kernel/nCic.ml
@@ -105,7 +105,7 @@ type ind_pragma = (* pragmatic of the object *)
    * fields names and if they are coercions and then the coercion arity *)
 
 type source = [ `Generated (* generated by matita *)
-              | `Provided  (* provided by the user directly or from another ITP *)
+              | `Provided  (* provided as defined by the user *)
               | `Implied   (* provided as generated by another ITP *)
               ]