X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fng_kernel%2FnCic.ml;fp=matitaB%2Fcomponents%2Fng_kernel%2FnCic.ml;h=c08f4ed04ee11cfbe4fe60c09c2488522e89a0bf;hb=928af763320668168206e88d93e8a77698f3b925;hp=271bf52842494ef50518e158ad8a3db8a7526522;hpb=c9c6cae5121a25b05450ea42578f14f74569cfbf;p=helm.git

diff --git a/matitaB/components/ng_kernel/nCic.ml b/matitaB/components/ng_kernel/nCic.ml
index 271bf5284..c08f4ed04 100644
--- a/matitaB/components/ng_kernel/nCic.ml
+++ b/matitaB/components/ng_kernel/nCic.ml
@@ -94,6 +94,7 @@ type def_pragma = (* pragmatic of the object *)
   | `Elim of sort       (* elimination principle; universe is not relevant *)
   | `Projection         (* record projection *)
   | `InversionPrinciple (* inversion principle *)
+  | `DiscriminationPrinciple (* discrimination principle *)
   | `Variant 
   | `Local 
   | `Regular ]            (* Local = hidden technicality *)