let interpretate ~context ~env ast =
let rec aux loc context = function
- | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
+ | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) ->
+ aux loc context term
+ | CicTextualParser2Ast.AttributedTerm (_, term) -> aux loc context term
| CicTextualParser2Ast.Appl terms ->
Cic.Appl (List.map (aux loc context) terms)
| CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
| Some term -> aux loc context term
in
match ast with
- | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
+ | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) -> aux loc context term
| _ -> assert false
let domain_of_term ~context ast =
let rec aux loc context = function
- | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
+ | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) ->
+ aux loc context term
+ | CicTextualParser2Ast.AttributedTerm (_, term) -> aux loc context term
| CicTextualParser2Ast.Appl terms ->
List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
Domain.empty terms
| Some t -> aux loc context t
in
match ast with
- | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
+ | CicTextualParser2Ast.AttributedTerm (`Loc loc, term) -> aux loc context term
| _ -> assert false
module Make (C: Callbacks) =