metasenv,GrafiteAst.Assumption loc
| GrafiteAst.Auto (loc,params) ->
metasenv,GrafiteAst.Auto (loc,params)
+ | GrafiteAst.Cases (loc, what, idents) ->
+ let metasenv,what = disambiguate_term context metasenv what in
+ metasenv,GrafiteAst.Cases (loc, what, idents)
| GrafiteAst.Change (loc, pattern, with_what) ->
let with_what = disambiguate_lazy_term with_what in
let pattern = disambiguate_pattern pattern in
metasenv,(GrafiteAst.Type (uri, tyno) :: types)
| _ ->
raise (GrafiteDisambiguator.DisambiguationError
- (0,[[[],[],None,lazy "Decompose works only on inductive types"]])))
+ (0,[[[],[],None,lazy "Decompose works only on inductive types",true]])))
in
let metasenv,types =
List.fold_left disambiguate (metasenv,[]) types
let metasenv,cic =
match term1 with
None -> metasenv,None
- | Some t ->
+ | Some (start,t) ->
let metasenv,t = disambiguate_term context metasenv t in
- metasenv,Some t in
+ metasenv,Some (start,t) in
let metasenv,cic'= disambiguate_term context metasenv term2 in
let metasenv,cic'' =
match term3 with