X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAst.ml;h=fab264d0798748b842c00733245074af5930cc33;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;hp=ae9143dabf849ed29f1d9c5c9e41b2f8114c9230;hpb=bc36fe01d5465d07ef76c445c83639e341f3eb2a;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index ae9143dab..fab264d07 100644
--- 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,
@@ -99,13 +100,13 @@ type 'term macro =
   | WLocate of loc * string
   | WElim of loc * 'term
   (* real macros *)
-  | Abort of loc
+(*   | Abort of loc *)
   | Print of loc * string
   | Check of loc * 'term 
   | Hint of loc
   | 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 *)
@@ -115,23 +116,30 @@ type alias_spec =
   | Symbol_alias of string * int * string (* name, instance no, description *)
   | Number_alias of int * string          (* instance no, description *)
 
-type 'term command =
-  | Set of loc * string * string
-  | Qed of loc
-      (** name.
-       * Name is needed when theorem was started without providing a name
-       *)
-  | Inductive of loc * (string * 'term) list * 'term inductive_type list
+type obj =
+  | Inductive of (string * CicAst.term) list * CicAst.term inductive_type list
       (** parameters, list of loc * mutual inductive types *)
-  | Theorem of loc * thm_flavour * string option * 'term * 'term option
+  | Theorem of thm_flavour * string * CicAst.term * CicAst.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 * CicAst.term) list * string * CicAst.term *
+      (string * CicAst.term) list
+
+type ('term,'obj) command =
+  | Set of loc * string * string
+  | Qed of loc
+      (** name.
+       * Name is needed when theorem was started without providing a name
+       *)
   | Coercion of loc * 'term
   | Alias of loc * alias_spec
+      (** parameters, name, type, fields *) 
+  | Obj of loc * 'obj
 
 type ('term, 'ident) tactical =
   | Tactic of loc * ('term, 'ident) tactic
@@ -146,19 +154,19 @@ type ('term, 'ident) tactical =
   | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
 
 
-type ('term, 'ident) code =
-  | Command of loc * 'term command
+type ('term, 'obj, 'ident) code =
+  | Command of loc * ('term,'obj) command
   | Macro of loc * 'term macro 
       (* Macro are substantially queries, but since we are not the kind of
        * peolpe that like to push "start" to turn off the computer 
        * we added this command *)
   | Tactical of loc * ('term, 'ident) tactical
              
-type ('term, 'ident) comment =
+type ('term, 'obj, 'ident) comment =
   | Note of loc * string
-  | Code of loc * ('term, 'ident) code
+  | Code of loc * ('term, 'obj, 'ident) code
              
-type ('term, 'ident) statement =
-  | Executable of loc * ('term, 'ident) code
-  | Comment of loc * ('term, 'ident) comment
+type ('term, 'obj, 'ident) statement =
+  | Executable of loc * ('term, 'obj, 'ident) code
+  | Comment of loc * ('term, 'obj, 'ident) comment