| CicNotationPt.Ident _
| CicNotationPt.Uri _
| CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+ | CicNotationPt.NCic _ -> assert false
| CicNotationPt.NRef _ -> assert false
| CicNotationPt.Ident (name,subst)
| CicNotationPt.Uri (name, subst) as ast ->
let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
Cic.InductiveDefinition
(tyl,[],List.length params,[`Class (`Record field_names)])
- | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+ | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) ->
let attrs = [`Flavour flavour] in
let ty' = interpretate_term [] env None false ty in
(match bo,flavour with