s/LocatedTerm/AnnotatedTerm + various annotations/

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index e8d3e58f15e303607496d1f82ada36d754de7fa5..b2b7149758731ea770afa671b135e54204c6a4a4 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -75,7 +75,9 @@ let find_in_environment name context =
 
 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) ->
@@ -190,12 +192,14 @@ let interpretate ~context ~env ast =
     | 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
@@ -269,7 +273,7 @@ let domain_of_term ~context ast =
     | 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) =