- New attribute `Implied put beside `Generated and `Provided.

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

diff --git a/matita/components/ng_kernel/nCicPp.ml b/matita/components/ng_kernel/nCicPp.ml
index 11ba55e787c0a192dfe53e3773f0e36ecc75cd1b..5a99a0664e111c40d2ca8de893d54185051ccb8d 100644 (file)
--- a/matita/components/ng_kernel/nCicPp.ml
+++ b/matita/components/ng_kernel/nCicPp.ml
@@ -263,6 +263,7 @@ let ppsubst status ~formatter ~metasenv ?(use_subst=true) subst =
 let string_of_generated = function
   | `Generated -> "Generated"
   | `Provided -> "Provided"
+  | `Implied -> "Implied"
 ;;
 
 let string_of_flavour = function