use uniform naming for referencing cicNotation* modules

[helm.git] / helm / ocaml / cic_notation / grafiteAst.ml

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index fb654529b8c354432493c422e4632fc5be7a271d..82d90498989cabec1ac8209a22b6042135649e8f 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -23,11 +23,13 @@
  * http://helm.cs.unibo.it/
  *)
 
+module Ast = CicNotationPt
+
 type direction = [ `LeftToRight | `RightToLeft ]
 type 'term reduction_kind =
  [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ]
 
-type loc = CicNotationPt.location
+type loc = Ast.location
 
 type ('term, 'ident) pattern = 'term option * ('ident * 'term) list * 'term
 
@@ -111,19 +113,19 @@ type alias_spec =
   | Number_alias of int * string          (* instance no, description *)
 
 type obj =
-  | Inductive of (string * CicNotationPt.term) list *
-      CicNotationPt.term inductive_type list
+  | Inductive of (string * Ast.term) list *
+      Ast.term inductive_type list
       (** parameters, list of loc * mutual inductive types *)
-  | Theorem of thm_flavour * string * CicNotationPt.term *
-      CicNotationPt.term option
+  | Theorem of thm_flavour * string * Ast.term *
+      Ast.term option
       (** flavour, name, type, body
        * - name is absent when an unnamed theorem is being proved, tipically in
        *   interactive usage
        * - body is present when its given along with the command, otherwise it
        *   will be given in proof editing mode using the tactical language
        *)
-  | Record of (string * CicNotationPt.term) list * string * CicNotationPt.term *
-      (string * CicNotationPt.term) list
+  | Record of (string * Ast.term) list * string * Ast.term *
+      (string * Ast.term) list
 
 type ('term,'obj) command =
   | Default of loc * string * UriManager.uri list
@@ -138,12 +140,12 @@ type ('term,'obj) command =
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
-  | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
-      int * CicNotationPt.term
+  | Notation of loc * direction option * Ast.term * Gramext.g_assoc *
+      int * Ast.term
       (* direction, l1 pattern, associativity, precedence, l2 pattern *)
   | Interpretation of loc *
-      string * (string * CicNotationPt.argument_pattern list) *
-        CicNotationPt.cic_appl_pattern
+      string * (string * Ast.argument_pattern list) *
+        Ast.cic_appl_pattern
       (* description (i.e. id), symbol, arg pattern, appl pattern *)
 
     (* DEBUGGING *)