]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/disambiguation/disambiguate.ml
Different aliases, better equality inferred.
[helm.git] / helm / software / components / disambiguation / disambiguate.ml
index 52411d6ed2abf458ef8706691419713ffb6eb6bc..f3ba95765274fcd5788b1dad2112177fa9e49ba8 100644 (file)
@@ -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) ->