- new syntax for let rec/corec with flavor specifier (tested on lambdadelta/ground_2/)

[helm.git] / matita / components / ng_cic_content / interpretations.ml

diff --git a/matita/components/ng_cic_content/interpretations.ml b/matita/components/ng_cic_content/interpretations.ml
index e2c8c76d0c53a4286b8fca9643507f00dacbcc69..47b1ac0630ed7814bd7ad989e790cfbc5a29b35c 100644 (file)
--- 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