X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FgrafiteAst.ml;h=fb654529b8c354432493c422e4632fc5be7a271d;hb=95977594b05ba0320784a445d480b3fe11ef4e55;hp=11fef69a1317558fe75ed27deedac7cfd4c48fa0;hpb=d43002dfc61afac676ea14bc6a1418e5ec0e3e9c;p=helm.git

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index 11fef69a1..fb654529b 100644
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -24,7 +24,8 @@
  *)
 
 type direction = [ `LeftToRight | `RightToLeft ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
+type 'term reduction_kind =
+ [ `Normalize | `Reduce | `Simpl | `Unfold of 'term option | `Whd ]
 
 type loc = CicNotationPt.location
 
@@ -54,7 +55,7 @@ type ('term, 'ident) tactic =
   | Exact of loc * 'term
   | Exists of loc
   | Fail of loc
-  | Fold of loc * reduction_kind * 'term * ('term, 'ident) pattern
+  | Fold of loc * 'term reduction_kind * 'term * ('term, 'ident) pattern
   | Fourier of loc
   | FwdSimpl of loc * string * 'ident list
   | Generalize of loc * ('term, 'ident) pattern * 'ident option
@@ -65,7 +66,7 @@ type ('term, 'ident) tactic =
   | LApply of loc * int option * 'term list * 'term * 'ident option
   | Left of loc
   | LetIn of loc * 'term * 'ident
-  | Reduce of loc * reduction_kind * ('term, 'ident) pattern 
+  | Reduce of loc * 'term reduction_kind * ('term, 'ident) pattern 
   | Reflexivity of loc
   | Replace of loc * ('term, 'ident) pattern * 'term
   | Rewrite of loc * direction * 'term * ('term, 'ident) pattern
@@ -137,9 +138,9 @@ type ('term,'obj) command =
   | Alias of loc * alias_spec
       (** parameters, name, type, fields *) 
   | Obj of loc * 'obj
-  | Notation of loc * CicNotationPt.term * Gramext.g_assoc * int *
-      CicNotationPt.term
-      (* level 1 pattern, associativity, precedence, level 2 pattern *)
+  | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc *
+      int * CicNotationPt.term
+      (* direction, l1 pattern, associativity, precedence, l2 pattern *)
   | Interpretation of loc *
       string * (string * CicNotationPt.argument_pattern list) *
         CicNotationPt.cic_appl_pattern