prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / ocaml / cic_transformations / tacticAst.ml

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 692d4679e85b012e6da2018d38815c7983b9fae0..7fabafda3e5f1707172048a54e7e327d7a3984e7 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -24,7 +24,7 @@
  *)
 
 type direction = [ `Left | `Right ]
-type reduction_kind = [ `Reduce | `Simpl | `Whd ]
+type reduction_kind = [ `Reduce | `Simpl | `Whd | `Normalize ]
 (* type 'term pattern = Pattern of 'term *)
 
   (* everywhere includes goal and hypotheses *)
@@ -60,6 +60,7 @@ type ('term, 'ident) tactic =
   | LetIn of loc * 'term * 'ident
 (*   | Named_intros of loc * 'ident list (* joined with Intros above *) *)
 (*   | Reduce of loc * reduction_kind * 'term pattern * 'ident option (* what, where *) *)
+  | ReduceAt of loc * reduction_kind * 'ident * 'term
   | Reduce of loc * reduction_kind * ('term list * 'term pattern) option
       (* kind, (what, where)
       * if second argument is None, reduction is applied to the current goal,
@@ -92,15 +93,20 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 type print_kind = [ `Env | `Coer ]
 
 type 'term macro = 
-  | Abort of loc
+  (* Whelp's stuff *)
+  | WHint of loc * 'term 
+  | WMatch of loc * 'term 
+  | WInstance of loc * 'term 
+  | WLocate of loc * string
+  | WElim of loc * 'term
+  (* real macros *)
+(*   | Abort of loc *)
   | Print of loc * string
   | Check of loc * 'term 
   | Hint of loc
-  | Match of loc * 'term 
-  | Instance of loc * 'term 
   | Quit of loc
-  | Redo of loc * int option
-  | Undo of loc * int option
+(*   | Redo of loc * int option
+  | Undo of loc * int option *)
 (*   | Print of loc * print_kind *)
   | Search_pat of loc * search_kind * string  (* searches with string pattern *)
   | Search_term of loc * search_kind * 'term  (* searches with term pattern *)