X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_cic_content%2Finterpretations.ml;h=47b1ac0630ed7814bd7ad989e790cfbc5a29b35c;hb=5832735b721c0bd8567c8f0be761a9136363a2a6;hp=e2c8c76d0c53a4286b8fca9643507f00dacbcc69;hpb=064980eacc2efe70ffee96134d75dfa37506fc36;p=helm.git diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml index e2c8c76d0..47b1ac063 100644 --- a/matita/components/ng_cic_content/interpretations.ml +++ b/matita/components/ng_cic_content/interpretations.ml @@ -646,9 +646,9 @@ let nmap_obj0 status ~idref (_, _, metasenv, subst, kind) = | None -> None in N.Theorem (n, ty, xbo, attrs) - | NCic.Inductive (is_ind, lno, itl, (_, `Regular)) -> + | NCic.Inductive (is_ind, lno, itl, (src, `Regular)) -> let captures, context = build_captures lno itl in - N.Inductive (captures, List.map (build_inductive is_ind lno context) itl) + N.Inductive (captures, List.map (build_inductive is_ind lno context) itl, src) | _ -> assert false (* NCic.Fixpoint (is_rec, ifl, _) -> *) let nmap_obj status = with_idrefs nmap_obj0 status