X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;fp=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=52411d6ed2abf458ef8706691419713ffb6eb6bc;hb=63b86fce8a75490b957e7301517b9006f58321b6;hp=354a737832bd15085e5ce8f89ec6f8fa25951cd0;hpb=1bff098f89787157818e2eb62acd6fcf4a2979d2;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 354a73783..52411d6ed 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -334,7 +334,7 @@ let domain_of_term ~context term =
 let domain_of_obj ~context ast =
  assert (context = []);
   match ast with
-   | Ast.Theorem (_,_,ty,bo) ->
+   | Ast.Theorem (_,_,ty,bo,_) ->
       domain_of_term [] ty
       @ (match bo with
           None -> []