Réorganisation des tclTHEN (cf dev/changements.txt)

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

1 files changed, 39 insertions, 41 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index afee5e2a9..c9f8aca31 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -5,32 +5,27 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+
+(*i $Id$ *)
+
 (*i*)
 open Environ
 open Evd
 open Names
 open Term
 open Util
+open Tacexpr
+open Rawterm
+open Genarg
 (*i*)
 
 (* This module defines the structure of proof tree and the tactic type. So, it
    is used by Proof_tree and Refiner *)
 
-type bindOcc = 
-  | Dep of identifier
-  | NoDep of int
-  | Com
-
-type 'a substitution = (bindOcc * 'a) list
-
 type pf_status =
   | Complete_proof
   | Incomplete_proof
 
-type hyp_location = (* To distinguish body and type of local defs *)
-  | InHyp of identifier
-  | InHypType of identifier
-
 type prim_rule =
   | Intro of identifier
   | Intro_replacing of identifier
@@ -61,12 +56,11 @@ type 'a sigma = {
 type proof_tree = {
   status : pf_status;
   goal : goal;
-  ref : (rule * proof_tree list) option; 
-  subproof : proof_tree option }
+  ref : (rule * proof_tree list) option }
 
 and rule =
   | Prim of prim_rule
-  | Tactic of tactic_expression
+  | Tactic of tactic_expr * proof_tree
   | Change_evars
 
 and goal = evar_info
@@ -75,31 +69,35 @@ and tactic = goal sigma -> (goal list sigma * validation)
 
 and validation = (proof_tree list -> proof_tree)
 
+and tactic_expr =
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_tactic_expr
+
+and atomic_tactic_expr =
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_atomic_tactic_expr
+
 and tactic_arg =
-  | Command        of Coqast.t
-  | Constr         of constr
-  | OpenConstr     of Pretyping.open_constr
-  | Constr_context of constr
-  | Identifier     of identifier
-  | Qualid         of Nametab.qualid
-  | Integer        of int
-  | Clause         of hyp_location list
-  | Bindings       of Coqast.t substitution
-  | Cbindings      of constr   substitution 
-  | Quoted_string  of string
-  | Tacexp         of Coqast.t
-  | Tac            of tactic * Coqast.t
-  | Redexp         of Tacred.red_expr
-  | 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 =
-  | WildPat
-  | 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
+  (constr,
+   Closure.evaluable_global_reference,
+   inductive or_metanum,
+   identifier)
+     Tacexpr.gen_tactic_arg
+
+type hyp_location = identifier Tacexpr.raw_hyp_location
+
+type open_generic_argument =
+    (constr,raw_tactic_expr) generic_argument
+type closed_generic_argument =
+    (constr,raw_tactic_expr) generic_argument
+
+type 'a closed_abstract_argument_type =
+    ('a,constr,raw_tactic_expr) abstract_argument_type
+
+type declaration_hook = Nametab.strength -> Nametab.global_reference -> unit