X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=f27c723b0692eceb453084b52e47fd25758d66dd;hb=5832735b721c0bd8567c8f0be761a9136363a2a6;hp=58e600a425e6af9bbf437aa57e42e2f7afa9a11b;hpb=064980eacc2efe70ffee96134d75dfa37506fc36;p=helm.git

diff --git a/matita/components/disambiguation/disambiguate.ml b/matita/components/disambiguation/disambiguate.ml
index 58e600a42..f27c723b0 100644
--- a/matita/components/disambiguation/disambiguate.ml
+++ b/matita/components/disambiguation/disambiguate.ml
@@ -315,7 +315,7 @@ let domain_of_obj ~context ast =
       @ (match bo with
           None -> []
         | Some bo -> domain_of_term [] bo)
-   | Ast.Inductive (params,tyl) ->
+   | Ast.Inductive (params,tyl,_) ->
       let context, dom = 
        List.fold_left
         (fun (context, dom) (var, ty) ->
@@ -335,7 +335,7 @@ let domain_of_obj ~context ast =
                List.map
                 (fun (_,ty) -> domain_of_term context_w_types ty) cl))
                 tyl)
-   | Ast.Record (params,var,ty,fields) ->
+   | Ast.Record (params,var,ty,fields,_) ->
       let context, dom = 
        List.fold_left
         (fun (context, dom) (var, ty) ->