s/LocatedTerm/AnnotatedTerm + various annotations/

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2Ast.mli

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli
index 1b5933f7dd3be255222487e3e8993dde68f027fd..849d102850966e7d80d09ba918108b2b5d1db2ce 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Ast.mli
@@ -63,8 +63,13 @@ type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
 type induction_kind = [ `Inductive | `CoInductive ]
 type sort_kind = [ `Prop | `Set | `Type | `CProp ]
 
+type term_attribute =
+  [ `Loc of location  (* source file location *)
+  | `IdRef of string  (* ACic pointer *)
+  ]
+
 type term =
-  | LocatedTerm of location * term
+  | AttributedTerm of term_attribute * term
 
   | Appl of term list
   | Appl_symbol of string * int * term list (* literal, instance, args *)