Big commit and major code clean-up:

[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 9023b48692c85aa578f8dcd118f93bf030bc0548..fab264d0798748b842c00733245074af5930cc33 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -116,25 +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 *) 
-  | Record of loc * (string * 'term) list * string * 'term * (string * 'term) list
+  | Obj of loc * 'obj
 
 type ('term, 'ident) tactical =
   | Tactic of loc * ('term, 'ident) tactic
@@ -149,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