| 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))