| 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 ->
CicEnvironment.CircularDependency _ ->
raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
| CicNotationPt.Implicit `Vector -> assert false
- | CicNotationPt.Implicit `JustOne -> Cic.Implicit None
+ | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None
| CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
| CicNotationPt.Num (num, i) ->
Disambiguate.resolve ~mk_choice ~env
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