- | GrafiteAst.Decompose (loc, types, what, names) ->
- let disambiguate (metasenv,types) = function
- | GrafiteAst.Type _ -> assert false
- | GrafiteAst.Ident id ->
- (match
- disambiguate_term context metasenv
- (CicNotationPt.Ident(id, None))
- with
- | metasenv,Cic.MutInd (uri, tyno, _) ->
- metasenv,(GrafiteAst.Type (uri, tyno) :: types)
- | _ ->
- raise (GrafiteDisambiguator.DisambiguationError
- (0,[[[],[],None,lazy "Decompose works only on inductive types"]])))
- in
- let metasenv,types =
- List.fold_left disambiguate (metasenv,[]) types
- in
- metasenv,GrafiteAst.Decompose (loc, types, what, names)
+ | GrafiteAst.Decompose (loc, names) ->
+ metasenv,GrafiteAst.Decompose (loc, names)