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
- None -> metasenv,None
- | Some t ->
+ `Auto _ as t -> metasenv,t
+ | `Term t ->
let metasenv,t = disambiguate_term context metasenv t in
- metasenv,Some t in
+ metasenv,`Term t in
metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)