added a lot of notation: arithmetic operators, relational operators, ...

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 06f18080d07466aaccba41ca71b3d83599ae4678..ca5f1449c961826f35516c629c59f23ec7402079 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -63,7 +63,9 @@ let refine metasenv context term =
         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 =
@@ -274,10 +276,15 @@ let domain_of_term ~context ast =
     | 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