X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicPp.ml;h=5a99a0664e111c40d2ca8de893d54185051ccb8d;hb=b3afed9fd3cc38ecd4578f6b0741be50872a2828;hp=0d78c4971bd90ff46364aaef74dc6330d78b4f7d;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/ng_kernel/nCicPp.ml b/matita/components/ng_kernel/nCicPp.ml
index 0d78c4971..5a99a0664 100644
--- 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
@@ -280,6 +281,7 @@ let string_of_pragma = function
   | `Elim _sort -> "Elim _"
   | `Projection -> "Projection"
   | `InversionPrinciple -> "InversionPrinciple"
+  | `DiscriminationPrinciple -> "DiscriminationPrinciple"
   | `Variant -> "Variant"
   | `Local -> "Local"
   | `Regular -> "Regular"