X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationUtil.ml;h=d9114b1808b1b5cca3da1736977718953b8adc57;hb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;hp=8e487ed11ed293374f4737a39bbc0e975b0165ff;hpb=4104453c74bbff05f95003f8d6239f873d1adbf9;p=helm.git

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index 8e487ed11..d9114b180 100644
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -366,7 +366,7 @@ let freshen_obj obj =
   let index = ref 0 in
   let freshen_term = freshen_term ~index in
   let freshen_name_ty = List.map (fun (n, t) -> (n, freshen_term t)) in
-  let freshen_name_ty_b = List.map (fun (n, t, b) -> (n, freshen_term t, b)) in
+  let freshen_name_ty_b = List.map (fun (n,t,b,i) -> (n,freshen_term t,b,i)) in
   match obj with
   | CicNotationPt.Inductive (params, indtypes) ->
       let indtypes =