X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=e2c8c76d0c53a4286b8fca9643507f00dacbcc69;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=741cfa64043e919c5b87b2331604da0012a7176c;hpb=225887a9f23aac79d4cca907da026917b7df04dc;p=helm.git

diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index 741cfa640..e2c8c76d0 100644
--- a/matita/components/ng_cic_content/interpretations.ml
+++ b/matita/components/ng_cic_content/interpretations.ml
@@ -639,13 +639,13 @@ let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) =
       n, is_ind, ty, List.map (build_constractor lno context) cl
    in
    match kind with
-      | NCic.Constant (_, n, xbo, ty, (_, flavour, pragma)) ->
+      | NCic.Constant (_, n, xbo, ty, attrs) ->
 	 let ty = nast_of_cic ~context:[] ty in
          let xbo = match xbo with 
 	    | Some bo -> Some (nast_of_cic ~context:[] bo)
 	    | None    -> None
 	 in
-	 N.Theorem (flavour, n, ty, xbo, pragma)
+	 N.Theorem (n, ty, xbo, attrs)
       | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) ->      
          let captures, context = build_captures lno itl in
 	 N.Inductive (captures, List.map (build_inductive is_ind lno context) itl)