Ko
let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
- snd (Environment.find item env) env num args
+ try
+ snd (Environment.find item env) env num args
+ with Not_found -> assert false
(* TODO move it to Cic *)
let find_in_environment name context =
| CicAst.AttributedTerm (_, term) -> aux loc context term
| CicAst.Appl terms ->
List.fold_left (fun dom term -> aux loc context term @ dom) [] terms
- | CicAst.Binder (_, (var, typ), body) ->
+ | CicAst.Binder (kind, (var, typ), body) ->
+ let kind_dom =
+ match kind with
+ | `Exists -> [ Symbol ("exists", 0) ]
+ | _ -> []
+ in
let type_dom = aux_option loc context typ in
let body_dom = aux loc (var :: context) body in
- body_dom @ type_dom
+ body_dom @ type_dom @ kind_dom
| CicAst.Case (term, indty_ident, outtype, branches) ->
let term_dom = aux loc context term in
let outtype_dom = aux_option loc context outtype in