| GrafiteAst.Cut (loc, ident, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Cut (loc, ident, cic)
- | 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",true]])))
- 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)
| GrafiteAst.Demodulate loc ->
metasenv,GrafiteAst.Demodulate loc
| GrafiteAst.Destruct (loc,term) ->