| CicNotationPt.Theorem (flavour, name, ty, bo) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
- (match bo with
- None ->
+ (match bo,flavour with
+ None,`Axiom ->
+ Cic.Constant (name,None,ty',[],attrs)
+ | Some bo,`Axiom -> assert false
+ | None,_ ->
Cic.CurrentProof (name,[],Cic.Implicit None,ty',[],attrs)
- | Some bo ->
+ | Some bo,_ ->
let bo' = Some (interpretate_term [] env None false bo) in
Cic.Constant (name,bo',ty',[],attrs))
(* dom1 \ dom2 *)
let domain_diff dom1 dom2 =
(* let domain_diff = Domain.diff *)
- let is_in_dom2 =
- List.fold_left (fun pred elt -> (fun elt' -> elt' = elt || pred elt'))
- (fun _ -> false) dom2
+ let is_in_dom2 elt =
+ List.exists
+ (function
+ | Symbol (symb, 0) ->
+ (match elt with
+ Symbol (symb',_) when symb = symb' -> true
+ | _ -> false)
+ | item -> elt = item
+ ) dom2
in
List.filter (fun (_,elt) -> not (is_in_dom2 elt)) dom1
| item -> item
in
Environment.find item e
- with Not_found -> [])
+ with Not_found -> lookup_in_library ())
in
choices
in