Ajout du langage de tactiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@401 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 83 deletions

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index f4990659c6..446d4b2a29 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -8,85 +8,9 @@ open Sign
 open Evd
 open Stamps
 open Environ
+open Proof_type
 open Typing
 
-type bindOcc = 
-  | Dep of identifier
-  | NoDep of int
-  | Com
-
-type 'a substitution = (bindOcc * 'a) list
-
-type tactic_arg =
-  | Command       of Coqast.t
-  | Constr        of constr
-  | Identifier    of identifier
-  | Integer       of int
-  | Clause        of identifier list
-  | Bindings      of Coqast.t substitution
-  | Cbindings     of constr   substitution 
-  | Quoted_string of string
-  | Tacexp        of Coqast.t
-  | Redexp        of string * Coqast.t list
-  | Fixexp        of identifier * int * Coqast.t
-  | Cofixexp      of identifier * Coqast.t
-  | Letpatterns   of int list option * (identifier * int list) list
-  | Intropattern  of intro_pattern
-
-and intro_pattern =
-  | IdPat   of identifier
-  | DisjPat of intro_pattern list
-  | ConjPat of intro_pattern list
-  | ListPat of intro_pattern list  
-
-and tactic_expression = string * tactic_arg list
-
-
-type pf_status = Complete_proof | Incomplete_proof
-
-type prim_rule_name = 
-  | Intro
-  | Intro_after
-  | Intro_replacing
-  | Fix
-  | Cofix
-  | Refine 
-  | Convert_concl
-  | Convert_hyp
-  | Thin
-  | Move of bool
-
-type prim_rule = {
-  name : prim_rule_name;
-  hypspecs : identifier list;
-  newids : identifier list;
-  params : Coqast.t list;
-  terms : constr list }
-
-type local_constraints = Intset.t
-
-type proof_tree = {
-  status : pf_status;
-  goal : goal;
-  ref : (rule * proof_tree list) option; 
-  subproof : proof_tree option }
-
-and goal = ctxtty evar_info
-
-and rule =
-  | Prim of prim_rule
-  | Tactic of tactic_expression
-  | Context of ctxtty
-  | Local_constraints of local_constraints
-
-and ctxtty = {
-  pgm    : constr option;
-  mimick : proof_tree option;
-  lc     : local_constraints } 
-
-type evar_declarations = ctxtty evar_map
-
-
 let is_bind = function
   | Bindings _ -> true
   | _ -> false
@@ -101,7 +25,7 @@ let mk_goal ctxt env cl =
 
 (* Functions on the information associated with existential variables  *)
 
-let mt_ctxt lc = { pgm = None; mimick = None; lc = lc }
+let mt_ctxt lc = { pgm = None; lc = lc }
 
 let get_ctxt gl = out_some gl.evar_info
 
@@ -109,10 +33,6 @@ let get_pgm gl = (out_some gl.evar_info).pgm
 
 let set_pgm pgm ctxt = { ctxt with pgm = pgm }
 
-let get_mimick gl = (out_some gl.evar_info).mimick
-
-let set_mimick mimick ctxt = { mimick = mimick; pgm = ctxt.pgm; lc = ctxt.lc }
-
 let get_lc gl = (out_some gl.evar_info).lc
 
 (* Functions on proof trees *)
@@ -442,7 +362,7 @@ let ast_of_cvt_arg = function
 	     (ast_of_cvt_bind
 		(ast_of_constr false (assumptions_for_print []))) bl)
   | Tacexp ast      -> ope ("TACTIC",[ast]) 
-  | Redexp (s,args) -> ope ("REDEXP", [ope(s,args)])
+  | Redexp red -> failwith "TODO: ast_of_cvt_arg: Redexp"
   | Fixexp (id,n,c) -> ope ("FIXEXP",[(nvar (string_of_id id)); 
                                       (num n); 
                                       ope ("COMMAND",[c])])