]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/ng_kernel/nCicPp.ml
Changes in "destruct" tactic (allowing performance improvements):
[helm.git] / matita / components / ng_kernel / nCicPp.ml
index 0d78c4971bd90ff46364aaef74dc6330d78b4f7d..11ba55e787c0a192dfe53e3773f0e36ecc75cd1b 100644 (file)
@@ -280,6 +280,7 @@ let string_of_pragma = function
   | `Elim _sort -> "Elim _"
   | `Projection -> "Projection"
   | `InversionPrinciple -> "InversionPrinciple"
+  | `DiscriminationPrinciple -> "DiscriminationPrinciple"
   | `Variant -> "Variant"
   | `Local -> "Local"
   | `Regular -> "Regular"