X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=f3ba95765274fcd5788b1dad2112177fa9e49ba8;hb=847f57ed13f0b281dc3f2aa84bd89252d1b6a989;hp=354a737832bd15085e5ce8f89ec6f8fa25951cd0;hpb=d34061fd1c820139fad38c39dee6377e5057bf26;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 354a73783..f3ba95765 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -311,6 +311,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
             [ Node ([loc], Id name, terms) ]))
   | Ast.Uri _ -> []
   | Ast.NRef _ -> []
+  | Ast.NCic _ -> []
   | Ast.Implicit _ -> []
   | Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
   | Ast.Meta (index, local_context) ->
@@ -334,7 +335,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 -> []