Ajout du langage de tactiques

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

23 files changed, 1127 insertions, 331 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index e02ffa3b8b..dd5ebb6ef4 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -10,7 +10,7 @@ open Sign
 open Instantiate
 open Environ
 open Evd
-open Proof_trees
+open Proof_type
 open Logic
 open Reduction
 open Tacmach
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 1f28a73afe..6354a34e37 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -6,7 +6,7 @@ open Util
 open Names
 open Term
 open Tacmach
-open Proof_trees
+open Proof_type
 (*i*)
 
 (* The Type of Constructions clausale environments. *)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 94f69474b7..91a83ea9d9 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -12,6 +12,7 @@ open Evd
 open Reduction
 open Typing
 open Proof_trees
+open Proof_type
 open Logic
 open Refiner
 
@@ -58,7 +59,6 @@ let extract_decl sp evc =
 
 let restore_decl sp evd evc =
   let newctxt = { lc = (ts_it evc).focus;
-                  mimick = (get_mimick evd);
                   pgm = (get_pgm evd) } in
   let newgoal = { evar_env = evd.evar_env; 
 		  evar_concl = evd.evar_concl;
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 620c9c4b8c..1674f2f3ac 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -8,6 +8,7 @@ open Sign
 open Environ
 open Evd
 open Proof_trees
+open Proof_type
 open Refiner
 (*i*)
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 71e79a7913..3270177ee1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -12,6 +12,7 @@ open Environ
 open Reduction
 open Typing
 open Proof_trees
+open Proof_type
 open Typeops
 open Type_errors
 open Coqast
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 7df383a738..31f0b51999 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -7,7 +7,7 @@ open Term
 open Sign
 open Evd
 open Environ
-open Proof_trees
+open Proof_type
 (*i*)
 
 (* The primitive refiner. *)
diff --git a/proofs/macros.ml b/proofs/macros.ml
index de6132f36f..95da5702d5 100644
--- a/proofs/macros.ml
+++ b/proofs/macros.ml
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Term
-open Proof_trees
+open Proof_type
 open Libobject
 open Library
 open Coqast
diff --git a/proofs/macros.mli b/proofs/macros.mli
index c62f13c76c..a237d3fd73 100644
--- a/proofs/macros.mli
+++ b/proofs/macros.mli
@@ -4,7 +4,7 @@
 (*i*)
 open Names
 open Tacmach
-open Proof_trees
+open Proof_type
 (*i*)
 
 (* This file contains the table of macro tactics. The body of the
diff --git a/proofs/pattern.ml b/proofs/pattern.ml
index a30a829927..983154c80f 100644
--- a/proofs/pattern.ml
+++ b/proofs/pattern.ml
@@ -100,9 +100,12 @@ let head_of_constr_reference = function
 
  *)
 
+exception PatternMatchingFailure
+
 let constrain ((n : int),(m : constr)) sigma =
   if List.mem_assoc n sigma then
-    if eq_constr m (List.assoc n sigma) then sigma else error "somatch"
+    if eq_constr m (List.assoc n sigma) then sigma
+    else raise PatternMatchingFailure
   else 
     (n,m)::sigma
     
@@ -124,8 +127,6 @@ let memb_metavars m n =
 
 let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2
 
-exception PatternMatchingFailure
-
 let matches_core convert pat c = 
   let rec sorec stk sigma p t =
     let cT = whd_castapp t in
@@ -180,6 +181,9 @@ let matches_core convert pat c =
       | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) ->
 	  sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2
 
+      | PRef (RConst (sp1,ctxt1)), IsConst (sp2,ctxt2) 
+          when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma
+
       | PRef (RConst (sp1,ctxt1)), _ when convert <> None ->
 	  let (env,evars) = out_some convert in
 	  if is_conv env evars (mkConst (sp1,ctxt1)) cT then sigma
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index a8b8ba97ec..7ffb408786 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -14,6 +14,7 @@ open Declare
 open Typing
 open Tacmach
 open Proof_trees
+open Proof_type
 open Lib
 open Astterm
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 13f7b6c1c1..3499f9227b 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -8,7 +8,7 @@ open Term
 open Sign
 open Environ
 open Declare
-open Proof_trees
+open Proof_type
 open Tacmach
 (*i*)
 
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])]) 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 6aa76f617f..60ae9b4f4c 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -9,95 +9,11 @@ open Term
 open Sign
 open Evd
 open Environ
+open Proof_type
 (*i*)
 
-(* This module declares the structures of proof trees, global and
-   readable constraints, and a few utilities on these types *)
-
-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
-
-(*s Proof trees. 
-  [ref] = [None] if the goal has still to be proved, 
-  and [Some (r,l)] if the rule [r] was applied to the goal
-  and gave [l] as subproofs to be completed. 
-  [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; 
-  [p] is then the proof that the goal can be proven if the goals
-  in [l] are solved. *)
-
-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
-
+(* This module declares readable constraints, and a few utilities on
+   constraints and proof trees *)
 
 val mk_goal : ctxtty -> env -> constr -> goal
 
@@ -105,8 +21,6 @@ val mt_ctxt    : local_constraints -> ctxtty
 val get_ctxt   : goal -> ctxtty
 val get_pgm    : goal -> constr option
 val set_pgm    : constr option -> ctxtty -> ctxtty
-val get_mimick : goal -> proof_tree option
-val set_mimick : proof_tree option ->  ctxtty -> ctxtty
 val get_lc     : goal -> local_constraints
 
 val rule_of_proof     : proof_tree -> rule
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
new file mode 100644
index 0000000000..eaebd6b992
--- /dev/null
+++ b/proofs/proof_type.ml
@@ -0,0 +1,106 @@
+(*i*)
+open Environ
+open Evd
+open Names
+open Stamps
+open Term
+open Util
+(*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 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 ctxtty = {
+  pgm    : constr option;
+  lc     : local_constraints } 
+
+type evar_declarations = ctxtty evar_map
+
+(* A global constraint is a mappings of existential variables
+   with some extra information for the program tactic *)
+type global_constraints  = evar_declarations timestamped
+
+(*Signature useful to define the tactic type*)
+type 'a sigma = { 
+  it : 'a ; 
+  sigma : global_constraints }
+
+(*s Proof trees. 
+  [ref] = [None] if the goal has still to be proved, 
+  and [Some (r,l)] if the rule [r] was applied to the goal
+  and gave [l] as subproofs to be completed. 
+  [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; 
+  [p] is then the proof that the goal can be proven if the goals
+  in [l] are solved. *)
+type proof_tree = {
+  status : pf_status;
+  goal : goal;
+  ref : (rule * proof_tree list) option; 
+  subproof : proof_tree option }
+
+and rule =
+  | Prim of prim_rule
+  | Tactic of tactic_expression
+  | Context of ctxtty
+  | Local_constraints of local_constraints
+
+and goal = ctxtty evar_info
+
+and tactic = goal sigma -> (goal list sigma * validation)
+
+and validation = (proof_tree list -> proof_tree)
+
+and 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
+  | Tac           of tactic
+  | 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 =
+  | 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
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
new file mode 100644
index 0000000000..eaebd6b992
--- /dev/null
+++ b/proofs/proof_type.mli
@@ -0,0 +1,106 @@
+(*i*)
+open Environ
+open Evd
+open Names
+open Stamps
+open Term
+open Util
+(*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 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 ctxtty = {
+  pgm    : constr option;
+  lc     : local_constraints } 
+
+type evar_declarations = ctxtty evar_map
+
+(* A global constraint is a mappings of existential variables
+   with some extra information for the program tactic *)
+type global_constraints  = evar_declarations timestamped
+
+(*Signature useful to define the tactic type*)
+type 'a sigma = { 
+  it : 'a ; 
+  sigma : global_constraints }
+
+(*s Proof trees. 
+  [ref] = [None] if the goal has still to be proved, 
+  and [Some (r,l)] if the rule [r] was applied to the goal
+  and gave [l] as subproofs to be completed. 
+  [subproof] = [(Some p)] if [ref = (Some(Tactic t,l))]; 
+  [p] is then the proof that the goal can be proven if the goals
+  in [l] are solved. *)
+type proof_tree = {
+  status : pf_status;
+  goal : goal;
+  ref : (rule * proof_tree list) option; 
+  subproof : proof_tree option }
+
+and rule =
+  | Prim of prim_rule
+  | Tactic of tactic_expression
+  | Context of ctxtty
+  | Local_constraints of local_constraints
+
+and goal = ctxtty evar_info
+
+and tactic = goal sigma -> (goal list sigma * validation)
+
+and validation = (proof_tree list -> proof_tree)
+
+and 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
+  | Tac           of tactic
+  | 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 =
+  | 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
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 3af8748035..9e1698c25c 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -13,14 +13,9 @@ open Reduction
 open Instantiate
 open Type_errors
 open Proof_trees
+open Proof_type
 open Logic
 
-type 'a sigma = { 
-  it : 'a ; 
-  sigma : global_constraints }
-
-type validation = (proof_tree list -> proof_tree)
-type tactic = goal sigma -> (goal list sigma * validation)
 type transformation_tactic = proof_tree -> (goal list * validation)
 
 let hypotheses gl = gl.evar_env
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 4d1edc7e5b..d0b3ca33ab 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -5,14 +5,11 @@
 open Term
 open Sign
 open Proof_trees
+open Proof_type
 (*i*)
 
 (* The refiner (handles primitive rules and high-level tactics). *)
 
-type 'a sigma = { 
-  it : 'a ; 
-  sigma : global_constraints }
-
 val sig_it  : 'a sigma -> 'a
 val sig_sig : 'a sigma -> global_constraints
 
@@ -23,10 +20,6 @@ val repackage : global_constraints ref -> 'a -> 'a sigma
 val apply_sig_tac :
   global_constraints ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
 
-type validation = (proof_tree list -> proof_tree)
-
-type tactic = goal sigma -> (goal list sigma * validation)
-
 type transformation_tactic = proof_tree -> (goal list * validation)
 
 val add_tactic             : string -> (tactic_arg list -> tactic) -> unit
diff --git a/proofs/stock.ml b/proofs/stock.ml
new file mode 100644
index 0000000000..ef0feec952
--- /dev/null
+++ b/proofs/stock.ml
@@ -0,0 +1,147 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Library
+
+(* The pattern table for tactics. *)
+
+(* The idea is that we want to write tactic files which are only
+   "activated" when certain modules are loaded and imported.  Already,
+   the question of how to store the tactics is hard, and we will not
+   address that here.  However, the question arises of how to store
+   the patterns that we will want to use for term-destructuring, and
+   the solution proposed is that we will store patterns with a
+   "module-marker", telling us which modules have to be open in order
+   to use the pattern.  So we will write:
+
+   let mark = make_module_marker ["<module-name>";<module-name>;...]
+
+   let p1 = put_pat mark "<parseable pattern goes here>"
+
+   And now, we can use:
+
+             (get p1)
+
+   to get the term which corresponds to this pattern, already parsed
+   and with the global names adjusted.
+
+   In other words, we will have the term which we would have had if we
+   had done an:
+
+        constr_of_com mt_ctxt (initial_sign()) "<text here>"
+
+   except that it will be computed at module-opening time, rather than
+   at tactic-application time.  The ONLY difference will be that
+   no implicit syntax resolution will happen.
+
+   So the entries we provide are:
+
+   type module_mark
+
+   value make_module_marker : string list -> module_mark
+
+   type marked_term
+
+   value put_pat : module_mark -> string -> marked_term
+
+   value get_pat : marked_term -> constr
+
+ *)
+
+type module_mark = Mmk of int
+
+let path_mark_bij = ref (Bij.empty : (string list,module_mark) Bij.t)
+
+let mmk_ctr = ref 0
+
+let new_mmk () = (incr mmk_ctr; !mmk_ctr)
+
+let make_module_marker sl =
+  let sorted_sl = Sort.list (<) sl in 
+  try 
+    Bij.map !path_mark_bij sorted_sl
+  with Not_found -> begin
+    let mmk = Mmk(new_mmk()) in 
+    path_mark_bij := Bij.add !path_mark_bij (sorted_sl,mmk);
+    mmk
+  end
+      
+let mark_satisfied mmk =
+  let spl = Bij.pam !path_mark_bij mmk in 
+  list_subset spl (loaded_modules())
+
+(* src_tab: for each module_mark, stores the tickets of objects which
+   need to be compiled when that mark becomes active.
+
+   obj_tab: for each ticket, stores the (possibly nonexistent)
+   compiled object
+
+   ticket_tab: for each ticket, stores its module_mark and the string
+   (source)
+
+   string_tab: for each string * module_mark, stores the ticket. *)
+
+type 'a stock_args = {
+  name : string;
+  proc : string -> 'a }
+
+type 'a stock = {
+  mutable src_tab : (module_mark,int) Gmapl.t;
+  mutable obj_tab : (int,'a) Gmap.t;
+  mutable ticket_string_bij : (int,string * module_mark) Bij.t;
+  args : 'a stock_args }
+
+type 'a stocked = int
+
+let stock_ctr = ref 0
+
+let new_stock () = (incr stock_ctr; !stock_ctr)
+
+let make_stock args =
+  { src_tab = Gmapl.empty;
+    obj_tab = Gmap.empty;
+    ticket_string_bij = Bij.empty;
+    args = args }
+  
+let stock stock mmk s =
+  try 
+    Bij.pam stock.ticket_string_bij (s,mmk)
+  with Not_found -> begin
+    let idx = new_stock() in 
+    stock.src_tab <- Gmapl.add mmk idx stock.src_tab;
+    stock.ticket_string_bij <- Bij.add stock.ticket_string_bij (idx,(s,mmk));
+    idx
+  end
+
+let pr_mm mm =
+  let sl = Bij.pam !path_mark_bij mm in
+  prlist_with_sep pr_spc (fun s -> [< 'sTR s >]) sl
+
+(* TODO: traiter a part les erreurs provenant de stock.args.proc
+   ( = parsing quand [so]pattern appelle retrieve)
+    -> eviter d'avoir l'erreur stocked datum *)
+
+let retrieve stock idx =
+  try 
+    Gmap.find idx stock.obj_tab
+  with Not_found ->
+    let (s,mmk) = Bij.map stock.ticket_string_bij idx in 
+    if mark_satisfied mmk then
+      try
+        let c = stock.args.proc s in 
+	stock.obj_tab <- Gmap.add idx c stock.obj_tab;
+        c
+      with e -> begin
+        mSGNL [< 'sTR"Processing of the stocked datum " ; 'sTR s ;
+                 'sTR" failed." ; 'fNL;
+                 Library.fmt_modules_state() >];
+	raise e
+      end
+    else
+      errorlabstrm "Stock.retrieve"
+        [< 'sTR"The stocked object "; 'sTR s; 'sTR" was not compilable"; 
+	   'fNL; 'sTR"Its module mark was: "; pr_mm mmk ; 'fNL ;
+           Library.fmt_modules_state() >]
diff --git a/proofs/stock.mli b/proofs/stock.mli
new file mode 100644
index 0000000000..c0cd43c7d5
--- /dev/null
+++ b/proofs/stock.mli
@@ -0,0 +1,24 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+(*i*)
+
+(* Module markers. *)
+
+type 'a stock
+
+type module_mark
+
+type 'a stocked
+
+type 'a stock_args = {
+  name : string;
+  proc : string -> 'a }
+
+val make_stock : 'a stock_args -> 'a stock
+val make_module_marker : string list -> module_mark
+val stock : 'a stock -> module_mark -> string -> 'a stocked
+val retrieve : 'a stock -> 'a stocked -> 'a
+
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 9e6f3006ea..0343895491 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -1,134 +1,703 @@
 
 (* $Id$ *)
 
+open Astterm
+open Closure
+open Generic
+open Libobject
+open Pattern
 open Pp
+open Rawterm
+open Sign
+open Tacred
 open Util
 open Names
-open Term
-open Proof_trees
+open Proof_type
 open Tacmach
 open Macros
 open Coqast
 open Ast
+open Term
 
+let err_msg_tactic_not_found macro_loc macro =
+  user_err_loc
+    (macro_loc,"macro_expand",
+     [< 'sTR"Tactic macro ";'sTR macro; 'sPC; 'sTR"not found" >])
 
-let tactic_tab = 
-  (Hashtbl.create 17 : (string, tactic_arg list -> tactic) Hashtbl.t)
+(*Values for interpretation*)
+type value=
+   VTactic of tactic
+  |VFTactic of tactic_arg list*(tactic_arg list->tactic)
+  |VRTactic of (goal list sigma * validation)
+  |VArg of tactic_arg
+  |VFun of (string*value) list*string option list*Coqast.t
+  |VVoid
+  |VRec of value ref;;
 
-let tacinterp_add (s,f) =
-  try 
-    Hashtbl.add tactic_tab s f
-  with Failure _ ->
-    errorlabstrm "tacinterp_add"
-      [< 'sTR"Cannot add the tactic " ; 'sTR s ; 'sTR" twice" >]
-      
-let overwriting_tacinterp_add (s,f) =
-  if Hashtbl.mem tactic_tab s then begin
-    Hashtbl.remove tactic_tab s;
-    warning ("Overwriting definition of tactic interpreter command "^s)
-  end;
-  Hashtbl.add tactic_tab s f
+(*Gives the identifier corresponding to an Identifier tactic_arg*)
+let id_of_Identifier=function
+   Identifier id -> id
+  |_ ->
+    anomalylabstrm "id_of_IDENTIFIER" [<'sTR "Not an IDENTIFIER tactic_arg">];;
 
-let tacinterp_init () = Hashtbl.clear tactic_tab
+(*Gives the constr corresponding to a Constr tactic_arg*)
+let constr_of_Constr=function
+   Constr c -> c
+  |_ -> anomalylabstrm "constr_of_Constr" [<'sTR "Not a CONSTR tactic_arg">];;
 
-let tacinterp_map s = Hashtbl.find tactic_tab s
+(*Signature for interpretation: val_interp and interpretation functions*)
+type interp_sign=
+  evar_declarations*Environ.env*(string*value) list*(int*constr) list*
+    goal sigma option;;
 
-let err_msg_tactic_not_found macro_loc macro =
-  user_err_loc
-    (macro_loc,"macro_expand",
-     [< 'sTR"Tactic macro ";'sTR macro; 'sPC; 'sTR"not found" >])
+(*Table of interpretation functions*)
+let interp_tab=
+  (Hashtbl.create 17:(string,interp_sign->Coqast.t->value) Hashtbl.t);;
+
+(*Adds an interpretation function*)
+let interp_add (ast_typ,interp_fun)=
+  try
+    Hashtbl.add interp_tab ast_typ interp_fun
+  with
+     Failure _ ->
+       errorlabstrm "interp_add" [<'sTR
+         "Cannot add the interpretation function for "; 'sTR ast_typ; 'sTR
+         " twice">];;
+
+(*Adds a possible existing interpretation function*)
+let overwriting_interp_add (ast_typ,interp_fun)=
+  if Hashtbl.mem interp_tab ast_typ then
+    (Hashtbl.remove interp_tab ast_typ;
+    warning ("Overwriting definition of tactic interpreter command "^ast_typ));
+  Hashtbl.add interp_tab ast_typ interp_fun;;
+
+(*Finds the interpretation function corresponding to a given ast type*)
+let look_for_interp=Hashtbl.find interp_tab;;
+
+(*Globalizes the identifier*)
+let glob_nvar id=
+  try
+    Nametab.sp_of_id CCI id
+  with
+     Not_found -> error ("unbound variable "^(string_of_id id));;
+
+(*Summary and Object declaration*)
+let mactab=ref Gmap.empty;;
+
+let lookup id=Gmap.find id !mactab;;
+
+let init ()=mactab:=Gmap.empty in
+let freeze ()= !mactab in
+let unfreeze fs=mactab:=fs in
+   Summary.declare_summary "tactic-definition"
+        {Summary.freeze_function   = freeze;
+         Summary.unfreeze_function = unfreeze;
+         Summary.init_function     = init};;
+
+let (inMD,outMD)=
+  let add (na,td)=mactab:=Gmap.add na td !mactab in
+  let cache_md (_,(na,td))=add (na,td) in 
+    declare_object ("TACTIC-DEFINITION",
+       {cache_function=cache_md;
+        load_function=(fun _ -> ());
+        open_function=(fun _ -> ());
+        specification_function=(fun x -> x)});;
+
+(*Adds a Tactic Definition in the table*)
+let add_tacdef na vbody=
+  if Gmap.mem na !mactab then
+    errorlabstrm "Tacdef.add_tacdef" [<'sTR
+      "There is already a Tactic Definition named "; 'sTR na>]
+  else
+    let _=Lib.add_leaf (id_of_string na) OBJ (inMD (na,vbody))
+    in
+      mSGNL [<'sTR (na^" is defined")>];;
+
+(*Unboxes the tactic_arg*)
+let unvarg=function
+   VArg a -> a
+  |_ -> errorlabstrm "unvarg" [<'sTR "Not a tactic argument">];;
+
+(*Unboxes VRec*)
+let unrec=function
+   VRec v -> !v
+  |a -> a;;
+
+(*Unboxes REDEXP*)
+let unredexp=function
+   Redexp c -> c
+  |_ ->  errorlabstrm "unredexp" [<'sTR "Not a REDEXP tactic_arg">];;
+
+(*Reads the head of Fun*)
+let read_fun ast=
+  let rec read_fun_rec=function
+     Node(_,"VOID",[])::tl -> None::(read_fun_rec tl)
+    |Nvar(_,s)::tl -> (Some s)::(read_fun_rec tl)
+    |[] -> []
+    |_ ->
+      anomalylabstrm "Tacinterp.read_fun_rec" [<'sTR "Fun not well formed">]
+  in
+    match ast with
+       Node(_,"FUNVAR",l) -> read_fun_rec l
+      |_ ->
+        anomalylabstrm "Tacinterp.read_fun" [<'sTR "Fun not well formed">];;
+
+(*Reads the clauses of a Rec*)
+let rec read_rec_clauses=function
+   [] -> []
+  |Node(_,"RECCLAUSE",[Nvar(_,name);it;body])::tl ->
+    (name,it,body)::(read_rec_clauses tl)
+  |_ ->
+    anomalylabstrm "Tacinterp.read_rec_clauses" [<'sTR
+      "Rec not well formed">];;
+
+(*Associates variables with values and gives the remaining variables and
+  values*)
+let head_with_value (lvar,lval)=
+  let rec head_with_value_rec lacc=function
+     ([],[]) -> (lacc,[],[])
+    |(vr::tvr,ve::tve) ->
+      (match vr with
+          None -> head_with_value_rec lacc (tvr,tve)
+         |Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
+    |(vr,[]) -> (lacc,vr,[])
+    |([],ve) -> (lacc,[],ve)
+  in
+    head_with_value_rec [] (lvar,lval);;
+
+(*Type of hypotheses for a Match Context rule*)
+type match_context_hyps=
+   NoHypId of constr_pattern
+  |Hyp of string*constr_pattern;;
+
+(*Type of a Match rule for Match Context and Match*)
+type match_rule=
+   Pat of match_context_hyps list*constr_pattern*Coqast.t
+  |All of Coqast.t;;
+
+(*Gives the ast of a COMMAND ast node*)
+let ast_of_command=function
+   Node(_,"COMMAND",[c]) -> c
+  |ast ->
+    anomaly_loc (Ast.loc ast, "Tacinterp.ast_of_command",[<'sTR
+      "Not a COMMAND ast node: ";print_ast ast>]);;
+
+(*Reads the hypotheses of a Match Context rule*)
+let rec read_match_context_hyps evc env=function
+   Node(_,"MATCHCONTEXTHYPS",[pc])::tl ->
+     (NoHypId (snd (interp_constrpattern evc env (ast_of_command
+       pc))))::(read_match_context_hyps evc env tl)
+  |Node(_,"MATCHCONTEXTHYPS",[Nvar(_,s);pc])::tl ->
+     (Hyp (s,snd (interp_constrpattern evc env (ast_of_command
+       pc))))::(read_match_context_hyps evc env tl)
+  |ast::tl ->
+    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",[<'sTR
+      "Not a MATCHCONTEXTHYP ast node: ";print_ast ast>])
+  |[] -> [];;
+
+(*Reads the rules of a Match Context*)
+let rec read_match_context_rule evc env=function
+   Node(_,"MATCHCONTEXTRULE",[tc])::tl ->
+     (All tc)::(read_match_context_rule evc env tl)
+  |Node(_,"MATCHCONTEXTRULE",l)::tl ->
+     let rl=List.rev l
+     in
+       (Pat (read_match_context_hyps evc env (List.tl (List.tl rl)),snd
+         (interp_constrpattern evc env (ast_of_command (List.nth rl
+         1))),List.hd rl))::(read_match_context_rule evc env tl)
+  |ast::tl ->
+    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR
+      "Not a MATCHCONTEXTRULE ast node: ";print_ast ast>])
+  |[] -> [];;
+
+(*Reads the rules of a Match*)
+let rec read_match_rule evc env=function
+   Node(_,"MATCHRULE",[te])::tl ->
+     (All te)::(read_match_rule evc env tl)
+  |Node(_,"MATCHRULE",[com;te])::tl ->
+    (Pat ([],snd (interp_constrpattern evc env (ast_of_command
+      com)),te))::(read_match_rule evc env tl)
+  |ast::tl ->
+    anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_rule",[<'sTR
+      "Not a MATCHRULE ast node: ";print_ast ast>])
+  |[] -> [];;
+
+(*Transforms a type_judgment signature into a (string*constr) list*)
+let make_hyps hyps=
+  let lid=List.map string_of_id (ids_of_sign hyps)
+  and lhyp=List.map body_of_type (vals_of_sign hyps)
+  in
+    List.combine lid lhyp;;
+
+(*For Match Context and Match*)
+exception No_match;;
+exception Not_coherent_metas;;
+
+(*Verifies if the matched list is coherent with respect to lcm*)
+let rec verify_metas_coherence lcm=function
+   (num,csr)::tl ->
+     if (List.for_all
+           (fun (a,b) ->
+              if a=num then
+                eq_constr b csr
+              else
+                true) lcm) then
+       (num,csr)::(verify_metas_coherence lcm tl)
+     else
+       raise Not_coherent_metas
+  |[] -> [];;
+
+(*Tries to match a pattern and a constr*)
+let apply_matching pat csr=
+  try
+    (Pattern.matches pat csr)
+  with
+     PatternMatchingFailure -> raise No_match;;
+
+(*Tries to match one hypothesis with a list of hypothesis patterns*)
+let apply_one_hyp_context lmatch mhyps (idhyp,hyp)=
+  let rec apply_one_hyp_context_rec (idhyp,hyp) mhyps_acc=function
+     (Hyp (idpat,pat))::tl ->
+       (try
+          ([idpat,VArg (Identifier
+            (id_of_string idhyp))],verify_metas_coherence lmatch
+            (Pattern.matches pat hyp),mhyps_acc@tl)
+        with
+           PatternMatchingFailure|Not_coherent_metas ->
+             apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[Hyp
+               (idpat,pat)]) tl)
+    |(NoHypId pat)::tl ->
+      (try
+         ([],verify_metas_coherence lmatch (Pattern.matches pat
+           hyp),mhyps_acc@tl)
+       with
+           PatternMatchingFailure|Not_coherent_metas ->
+             apply_one_hyp_context_rec (idhyp,hyp) (mhyps_acc@[NoHypId pat])
+               tl)
+    |[] -> raise No_match
+  in
+    apply_one_hyp_context_rec (idhyp,hyp) [] mhyps;;
+
+(*Prepares the lfun list for constr substitutions*)
+let rec make_subs_list=function
+   (id,VArg (Identifier i))::tl ->
+     (id_of_string id,VAR i)::(make_subs_list tl)
+  |(id,VArg (Constr c))::tl ->
+    (id_of_string id,c)::(make_subs_list tl)
+  |e::tl -> make_subs_list tl
+  |[] -> [];;
+
+(*Interprets any expression*)
+let rec val_interp (evc,env,lfun,lmatch,goalopt) ast=
+(*  mSGNL [<print_ast ast>];*)
+
+(*mSGNL [<print_ast (Termast.bdize false (Pretty.assumptions_for_print []) ((reduction_of_redexp redexp) env evc c))>];*)
+
+  match ast with
+     Node(_,"APP",l) ->
+       let fv=val_interp (evc,env,lfun,lmatch,goalopt) (List.hd l)
+       and largs=
+         List.map (val_interp (evc,env,lfun,lmatch,goalopt)) (List.tl l)
+       in
+         app_interp evc env lfun lmatch goalopt fv largs ast
+    |Node(_,"FUN",l) -> VFun (lfun,read_fun (List.hd l),List.nth l 1)
+    |Node(_,"REC",l) -> rec_interp evc env lfun lmatch goalopt ast l
+    |Node(_,"LET",[Node(_,"LETDECL",l);u]) ->
+      let addlfun=let_interp evc env lfun lmatch goalopt ast l
+      in
+        val_interp (evc,env,(lfun@addlfun),lmatch,goalopt) u
+    |Node(_,"MATCHCONTEXT",lmr) ->
+      match_context_interp evc env lfun lmatch goalopt ast lmr
+    |Node(_,"MATCH",lmr) ->
+      match_interp evc env lfun lmatch goalopt ast lmr
+    |Node(_,"IDTAC",[]) -> VTactic tclIDTAC
+    |Node(_,"FAIL",[]) -> VTactic tclFAIL
+    |Node(_,"TACTICLIST",l) ->
+      VTactic (interp_semi_list tclIDTAC lfun lmatch l)
+    |Node(_,"DO",[n;tac]) ->
+      VTactic (tclDO (num_of_ast n) (tac_interp lfun lmatch tac))
+    |Node(_,"TRY",[tac]) ->
+      VTactic (tclTRY (tac_interp lfun lmatch tac))
+    |Node(_,"INFO",[tac]) ->
+      VTactic (tclINFO (tac_interp lfun lmatch tac))
+    |Node(_,"REPEAT",[tac]) ->
+      VTactic (tclREPEAT (tac_interp lfun lmatch tac))
+    |Node(_,"ORELSE",[tac1;tac2]) ->
+      VTactic (tclORELSE (tac_interp lfun lmatch tac1) (tac_interp lfun lmatch
+        tac2))
+    |Node(_,"FIRST",l) ->
+      VTactic (tclFIRST (List.map (tac_interp lfun lmatch) l))
+    |Node(_,"TCLSOLVE",l) ->
+      VTactic (tclSOLVE (List.map (tac_interp lfun lmatch) l))
+    |Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
+      val_interp (evc,env,lfun,lmatch,goalopt) (Node(loc0,"APP",[Node(loc1,
+        "PRIM-TACTIC",[Node(loc1,s,[])])]@l))
+    |Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) ->
+      VFTactic ([],(interp_atomic loc opn))
+    |Node(_,"VOID",[]) -> VVoid
+    |Nvar(_,s) ->
+       (try
+          (unrec (List.assoc s (List.rev lfun)))
+        with
+           Not_found ->
+             (try
+                (lookup s)
+              with
+                 Not_found -> VArg (Identifier (id_of_string s))))
+    |Str(_,s) -> VArg (Quoted_string s)
+    |Num(_,n) -> VArg (Integer n)
+    |Node(_,"COMMAND",[c]) -> com_interp (evc,env,lfun,lmatch,goalopt) c
+    |Node(_,"CASTEDCOMMAND",[c]) ->
+      cast_com_interp (evc,env,lfun,lmatch,goalopt) c
+    |Node(_,"BINDINGS",astl) ->
+      VArg (Cbindings (List.map (bind_interp evc env lfun lmatch goalopt)
+        astl))
+    |Node(_,"REDEXP",[Node(_,redname,args)]) ->
+      VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt)
+        (redname,args)))
+    |Node(_,"CLAUSE",cl) ->
+      VArg (Clause (List.map (fun ast -> id_of_Identifier (unvarg (val_interp
+        (evc,env,lfun,lmatch,goalopt) ast))) cl))
+    |Node(_,"TACTIC",[ast]) -> VArg (Tac (tac_interp lfun lmatch ast))
+(*Remains to treat*)
+    |Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
+      VArg ((Fixexp (id_of_string s,n,c)))
+    |Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) ->
+      VArg ((Cofixexp (id_of_string s,c)))
+(*End of Remains to treat*)
+    |Node(_,"INTROPATTERN", [ast]) ->
+      VArg ((Intropattern (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)
+        ast)))
+    |Node(_,"LETPATTERNS",astl) ->
+      VArg (Letpatterns (List.fold_left (cvt_letpattern
+        (evc,env,lfun,lmatch,goalopt)) (None,[]) astl))
+    |Node(loc,s,l) ->
+      (try
+         ((look_for_interp s) (evc,env,lfun,lmatch,goalopt) ast)
+       with
+          Not_found ->
+            val_interp (evc,env,lfun,lmatch,goalopt)
+              (Node(dummy_loc,"APPTACTIC",[ast])))
+    |_ ->
+      anomaly_loc (Ast.loc ast, "Tacinterp.val_interp",[<'sTR
+        "Unrecognizable ast: ";print_ast ast>])
+(*Interprets an application node*)
+and app_interp evc env lfun lmatch goalopt fv largs ast=
+  match fv with
+     VFTactic(l,f) -> VFTactic(l@(List.map unvarg largs),f)
+    |VFun(olfun,var,body) ->
+      let (newlfun,lvar,lval)=head_with_value (var,largs)
+      in
+        if lvar=[] then
+          if lval=[] then
+            val_interp (evc,env,(olfun@newlfun),lmatch,goalopt) body
+          else
+            app_interp evc env lfun lmatch goalopt (val_interp (evc,env,
+              (olfun@newlfun),lmatch,goalopt) body) lval ast
+        else
+          VFun(olfun@newlfun,lvar,body)
+    |_ ->
+      anomaly_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR
+        "Illegal application: "; print_ast ast>])
+(*Interprets recursive expressions*)
+and rec_interp evc env lfun lmatch goalopt ast=function
+   [Node(_,"RECCLAUSE",_)] as l ->
+     let (name,var,body)=List.hd (read_rec_clauses l)
+     and ve=ref VVoid
+     in
+       let newve=
+         VFun(lfun@[(name,VRec ve)],read_fun var,body)
+       in
+         ve:=newve;
+         !ve
+  |[Node(_,"RECDECL",l);u] ->
+    let lrc=read_rec_clauses l
+    in
+      let lref=Array.to_list (Array.make (List.length lrc) (ref VVoid))
+      in
+        let lenv=
+          List.fold_right2 (fun (name,_,_) vref l -> (name,VRec vref)::l) lrc
+            lref []
+        in
+          let lve=
+            List.map (fun (name,var,body) -> (name,VFun(lfun@lenv,read_fun
+              var,body))) lrc
+          in
+            List.iter2 (fun vref (_,ve) -> vref:=ve) lref lve;
+            val_interp (evc,env,(lfun@lve),lmatch,goalopt) u
+  |_ ->
+    anomaly_loc (Ast.loc ast, "Tacinterp.rec_interp",[<'sTR
+      "Rec not well formed: "; print_ast ast>])
+(*Interprets the clauses of a let*)
+and let_interp evc env lfun lmatch goalopt ast=function
+   [] -> []
+  |Node(_,"LETCLAUSE",[Nvar(_,id);t])::tl ->
+    (id,val_interp (evc,env,lfun,lmatch,goalopt) t)::(let_interp evc env lfun
+       lmatch goalopt ast tl)
+  |_ ->
+    anomaly_loc (Ast.loc ast, "Tacinterp.let_interp",[<'sTR
+      "Let not well formed: "; print_ast ast>])
+(*Interprets the Match Context expressions*)
+and match_context_interp evc env lfun lmatch goalopt ast lmr=
+  let rec apply_match_context evc env lfun lmatch goalopt=function
+     (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t
+    |(Pat (mhyps,mgoal,mt))::tl ->
+      (match goalopt with
+          None ->
+            errorlabstrm "Tacinterp.apply_match_context" [<'sTR
+              "No goal available">]
+         |Some g ->
+           let hyps=make_hyps (pf_hyps g)
+           and concl=pf_concl g
+           in
+             try
+               (let lgoal=apply_matching mgoal concl
+                in
+                  if mhyps=[] then
+                    val_interp (evc,env,lfun,lgoal@lmatch,goalopt) mt
+                  else
+                    apply_hyps_context evc env lfun lmatch g mt lgoal mhyps
+                      hyps)
+             with
+                No_match ->
+                  apply_match_context evc env lfun lmatch goalopt tl)
+    |_ ->
+      errorlabstrm "Tacinterp.apply_match_context" [<'sTR
+        "No matching clauses for Match Context">]
+  in
+    apply_match_context evc env lfun lmatch goalopt (read_match_context_rule
+      evc env lmr)
+(*Tries to match the hypotheses in a Match Context*)
+and apply_hyps_context evc env lfun_glob lmatch_glob goal mt lgmatch mhyps
+  hyps=
+  let rec apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt lfun
+    lmatch mhyps hyps hyps_acc=
+    match hyps with
+       hd::tl ->
+         (try
+            (let (lid,lm,newmhyps)=apply_one_hyp_context lmatch mhyps hd
+             in
+               if newmhyps=[] then
+                 match
+                   (val_interp (evc,env,(lfun@lid@lfun_glob),
+                     (lmatch@lm@lmatch_glob),Some goal) mt) with
+                    VTactic tac -> VRTactic (tac goal)
+                   |VFTactic (largs,f) -> VRTactic (f largs goal)
+                   |a -> a
+               else
+                 apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt
+                   (lfun@lid) (lmatch@lm) newmhyps (hyps_acc@tl) [])
+          with
+             No_match | _ ->
+               apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt
+                 lfun lmatch mhyps tl (hyps_acc@[hd]))
+      |[] -> raise No_match
+  in
+    apply_hyps_context_rec evc env lfun_glob lmatch_glob goal mt [] lgmatch
+      mhyps hyps []
+(*Interprets the Match expressions*)
+and match_interp evc env lfun lmatch goalopt ast lmr=
+  let rec apply_match evc env lfun lmatch goalopt csr=function
+     (All t)::tl -> val_interp (evc,env,lfun,lmatch,goalopt) t
+    |(Pat ([],mc,mt))::tl ->
+      (try
+         (let lcsr=apply_matching mc csr
+          in
+            val_interp (evc,env,lfun,(apply_matching mc csr)@lmatch,goalopt)
+              mt)
+       with
+          No_match -> apply_match evc env lfun lmatch goalopt csr tl)
+    |_ ->
+      errorlabstrm "Tacinterp.apply_match" [<'sTR
+        "No matching clauses for Match">]
+  in
+    let csr=
+      constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
+        (List.hd lmr)))
+    and ilr=read_match_rule evc env (List.tl lmr)
+    in
+      apply_match evc env lfun lmatch goalopt csr ilr
+(*Interprets tactic expressions*)
+and tac_interp lfun lmatch ast g=
+  let evc=project g
+  and env=pf_env g
+  in
+    match (val_interp (evc,env,lfun,lmatch,(Some g)) ast) with
+       VTactic tac -> (tac g)
+      |VFTactic (largs,f) -> (f largs g) 
+      |VRTactic res -> res
+      |_ ->
+        errorlabstrm "Tacinterp.interp_rec" [<'sTR
+          "Interpretation gives a non-tactic value">]
+(*Interprets a primitive tactic*)
+and interp_atomic loc opn args=vernac_tactic(opn,args)
+(*Interprets sequences of tactics*)
+and interp_semi_list acc lfun lmatch=function
+   (Node(_,"TACLIST",seq))::l ->
+     interp_semi_list (tclTHENS acc (List.map (tac_interp lfun lmatch) seq))
+       lfun lmatch l
+  |t::l ->
+    interp_semi_list (tclTHEN acc (tac_interp lfun lmatch t)) lfun lmatch l
+  |[] -> acc
+(*Interprets bindings for tactics*)
+and bind_interp evc env lfun lmatch goalopt=function
+   Node(_,"BINDING", [Num(_,n);Node(loc,"COMMAND",[c])]) ->
+     (NoDep n,constr_of_Constr (unvarg (val_interp
+       (evc,env,lfun,lmatch,goalopt) (Node(loc,"COMMAND",[c])))))
+  |Node(_,"BINDING", [Nvar(loc0,s); Node(loc1,"COMMAND",[c])]) -> 
+     (Dep (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
+       (Nvar(loc0,s))))),constr_of_Constr (unvarg (val_interp
+       (evc,env,lfun,lmatch,goalopt) (Node(loc1,"COMMAND",[c])))))
+  |Node(_,"BINDING", [Node(loc,"COMMAND",[c])]) ->
+    (Com,constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
+      (Node(loc,"COMMAND",[c])))))
+  |x ->
+    errorlabstrm "bind_interp" [<'sTR "Not the expected form in binding";
+      print_ast x>]
+(*Interprets a COMMAND expression*)
+and com_interp (evc,env,lfun,lmatch,goalopt)=function
+   Node(_,"EVAL",[c;rtc]) ->
+     let redexp=
+       unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc))
+     in
+       VArg (Constr ((reduction_of_redexp redexp) env evc (interp_constr1 evc
+         env (make_subs_list lfun) lmatch c)))
+  |c -> VArg (Constr (interp_constr1 evc env (make_subs_list lfun) lmatch c))
+(*Interprets a CASTEDCOMMAND expression*)
+and cast_com_interp (evc,env,lfun,lmatch,goalopt) com=
+  match goalopt with
+     Some gl ->
+       (match com with
+           Node(_,"EVAL",[c;rtc]) ->
+             let redexp=
+               unredexp (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) rtc))
+               in
+                 VArg (Constr ((reduction_of_redexp redexp) env evc
+                   (interp_casted_constr1 evc env (make_subs_list lfun) lmatch
+                   c (pf_concl gl))))
+          |c ->
+            VArg (Constr (interp_casted_constr1 evc env (make_subs_list lfun)
+              lmatch c (pf_concl gl))))
+    |None ->
+      errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
+and cvt_pattern (evc,env,lfun,lmatch,goalopt)=function
+    Node(_,"PATTERN", Node(loc,"COMMAND",[com])::nums) ->
+      let occs=List.map num_of_ast nums
+      and csr=
+        constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
+          (Node(loc,"COMMAND",[com]))))
+      in
+        let jdt=Typing.unsafe_machine env evc csr
+        in
+          (occs, jdt.Environ.uj_val, jdt.Environ.uj_type)
+  |arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
+and cvt_unfold (evc,env,lfun,lmatch,goalopt)=function
+   Node(_,"UNFOLD", com::nums) ->
+     (List.map num_of_ast nums,glob_nvar (id_of_Identifier (unvarg (val_interp
+       (evc,env,lfun,lmatch,goalopt) com))))
+  |arg -> invalid_arg_loc (Ast.loc arg,"cvt_unfold")
+(*Interprets the arguments of Fold*)
+and cvt_fold (evc,env,lfun,lmatch,goalopt)=function
+   Node(_,"COMMAND",[c]) as ast ->
+     constr_of_Constr (unvarg (val_interp (evc,env,lfun,lmatch,goalopt) ast))
+  |arg -> invalid_arg_loc (Ast.loc arg,"cvt_fold")
+(*Interprets the reduction flags*)
+and flag_of_ast (evc,env,lfun,lmatch,goalopt) lf=
+  let beta = ref false in
+  let delta = ref false in
+  let iota = ref false in
+  let idents = ref (None: (sorts oper -> bool) option) in
+  let set_flag = function
+      Node(_,"Beta",[]) -> beta := true
+    | Node(_,"Delta",[]) -> delta := true
+    | Node(_,"Iota",[]) -> iota := true
+    | Node(loc,"Unf",l) ->
+        if !delta then
+          if !idents = None then
+            let idl=
+              List.map (fun v -> glob_nvar (id_of_Identifier (unvarg
+                (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l
+            in
+              idents := Some
+                (function
+                     Const sp -> List.mem sp idl
+                   | Abst sp -> List.mem sp idl
+                   | _ -> false)
+          else user_err_loc(loc,"flag_of_ast",
+                  [< 'sTR"Cannot specify identifiers to unfold twice" >])
+        else user_err_loc(loc,"flag_of_ast",
+                  [< 'sTR"Delta must be specified before" >])
+    | Node(loc,"UnfBut",l) ->
+        if !delta then
+          if !idents = None then
+            let idl=
+              List.map (fun v -> glob_nvar (id_of_Identifier (unvarg
+                (val_interp (evc,env,lfun,lmatch,goalopt) v)))) l
+            in
+              idents := Some
+                (function
+                     Const sp -> not (List.mem sp idl)
+                   | Abst sp -> not (List.mem sp idl)
+                   | _ -> false)
+          else user_err_loc(loc,"flag_of_ast",
+                  [< 'sTR"Cannot specify identifiers to unfold twice" >])
+        else user_err_loc(loc,"flag_of_ast",
+                  [< 'sTR"Delta must be specified before" >])
+    | arg -> invalid_arg_loc (Ast.loc arg,"flag_of_ast")
+  in
+    List.iter set_flag lf;
+    { r_beta = !beta;
+      r_iota = !iota;
+      r_delta = match (!delta,!idents) with
+          (false,_) -> (fun _ -> false)
+        | (true,None) -> (fun _ -> true)
+        | (true,Some p) -> p }
+(*Interprets a reduction expression*)
+and redexp_of_ast (evc,env,lfun,lmatch,goalopt)=function
+  |("Red", []) -> Red
+  |("Hnf", []) -> Hnf
+  |("Simpl", []) -> Simpl
+  |("Unfold", ul) ->
+    Unfold (List.map (cvt_unfold (evc,env,lfun,lmatch,goalopt)) ul)
+  |("Fold", cl) -> Fold (List.map (cvt_fold (evc,env,lfun,lmatch,goalopt)) cl)
+  |("Cbv",lf) -> Cbv(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf)
+  |("Lazy",lf) -> Lazy(UNIFORM, flag_of_ast (evc,env,lfun,lmatch,goalopt) lf)
+  |("Pattern",lp) ->
+    Pattern (List.map (cvt_pattern (evc,env,lfun,lmatch,goalopt)) lp)
+  |(s,_) -> invalid_arg ("malformed reduction-expression: "^s)
+(*Interprets the patterns of Intro*)
+and cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)=function
+   Node(_,"IDENTIFIER", [Nvar(loc,s)]) ->
+     IdPat (id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
+       (Nvar (loc,s)))))
+  |Node(_,"DISJPATTERN", l) ->
+    DisjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l)
+  |Node(_,"CONJPATTERN", l) ->
+    ConjPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l)
+  |Node(_,"LISTPATTERN", l) ->
+    ListPat (List.map (cvt_intro_pattern (evc,env,lfun,lmatch,goalopt)) l)
+  |x ->
+    errorlabstrm "cvt_intro_pattern"
+      [<'sTR "Not the expected form for an introduction pattern!";print_ast
+      x>]
+(*Interprets a pattern of Let*)
+and cvt_letpattern (evc,env,lfun,lmatch,goalopt) (o,l)=function
+   Node(_,"HYPPATTERN", Nvar(loc,s)::nums) ->
+     (o,(id_of_Identifier (unvarg (val_interp (evc,env,lfun,lmatch,goalopt)
+       (Nvar (loc,s)))),List.map num_of_ast nums)::l)
+  |Node(_,"CCLPATTERN", nums) ->
+    if o<>None then
+      error "\"Goal\" occurs twice"
+    else
+      (Some (List.map num_of_ast nums), l)
+  |arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern");;
+
+(*Interprets tactic arguments*)
+let interp_tacarg sign ast=unvarg (val_interp sign ast);;
+
+(*Initial call for interpretation*)
+let interp=tac_interp [] [];;
 
-let cvt_bind = function
-  | Node(_,"BINDING", [Num(_,n); Node(_,"COMMAND",[c])]) -> (NoDep n,c)
-  | Node(_,"BINDING", [Nvar(_,s); Node(_,"COMMAND",[c])]) -> 
-      let id = id_of_string s in (Dep id,c)
-  | Node(_,"BINDING", [Node(_,"COMMAND",[c])]) -> (Com,c)
-  | x -> errorlabstrm "cvt_bind"
-        [< 'sTR "Not the expected form in binding!"; print_ast x >]
-	
-let rec cvt_intro_pattern = function
-  | Node(_,"IDENTIFIER", [Nvar(_,s)]) -> IdPat   (id_of_string s)
-  | Node(_,"DISJPATTERN", l) -> DisjPat (List.map cvt_intro_pattern l)
-  | Node(_,"CONJPATTERN", l) -> ConjPat (List.map cvt_intro_pattern l)
-  | Node(_,"LISTPATTERN", l) -> ListPat (List.map cvt_intro_pattern l)
-  | x -> errorlabstrm "cvt_intro_pattern"
-        [< 'sTR "Not the expected form for an introduction pattern!"; 
-            print_ast x >]
-
-let cvt_letpattern (o,l) = function
-  | Node(_,"HYPPATTERN", Nvar(_,s)::nums) ->
-      (o, (id_of_string s, List.map num_of_ast nums)::l)
-  | Node(_,"CCLPATTERN", nums) ->
-      if o<>None then error "\"Goal\" occurs twice"
-      else (Some (List.map num_of_ast nums), l)
-  | arg -> 
-      invalid_arg_loc (Ast.loc arg,"cvt_hyppattern")
-
-let cvt_letpatterns astl = List.fold_left cvt_letpattern (None,[]) astl
-
-let cvt_arg = function
-  | Nvar(_,s) -> 
-      Identifier (id_of_string s)
-  | Str(_,s) -> 
-      Quoted_string s
-  | Num(_,n) -> 
-      Integer n
-  | Node(_,"COMMAND",[c]) -> 
-      Command c
-  | Node(_,"BINDINGS",astl) -> 
-      Bindings (List.map cvt_bind astl)
-  | Node(_,"REDEXP",[Node(_,redname,args)]) -> 
-      Redexp (redname,args)
-  | Node(_,"CLAUSE",cl) -> 
-      Clause (List.map (compose id_of_string nvar_of_ast) cl)
-  | Node(_,"TACTIC",[ast]) -> 
-      Tacexp ast
-  | Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
-      Fixexp (id_of_string s,n,c)
-  | Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) ->
-      Cofixexp (id_of_string s,c)
-  | Node(_,"INTROPATTERN", [ast]) -> 
-      Intropattern (cvt_intro_pattern ast)
-  | Node(_,"LETPATTERNS", astl) -> 
-      let (o,l) = (cvt_letpatterns astl) in Letpatterns (o,l)
-  | x -> 
-      anomaly_loc (Ast.loc x, "Tacinterp.cvt_bind",
-                   [< 'sTR "Unrecognizable ast node : "; print_ast x >])
-
-let rec interp = function
-  | Node(loc,opn,tl) ->
-      (match (opn, tl) with
-         | ("TACTICLIST",_) -> interp_semi_list tclIDTAC tl
-	 | ("DO",[n;tac]) -> tclDO (num_of_ast n) (interp tac)
-	 | ("TRY",[tac]) -> tclTRY (interp tac)
-	 | ("INFO",[tac]) -> tclINFO (interp tac)
-	 | ("REPEAT",[tac]) -> tclREPEAT (interp tac)
-	 | ("ORELSE",[tac1;tac2]) -> tclORELSE (interp tac1) (interp tac2)
-	 | ("FIRST",l) -> tclFIRST (List.map interp l)
-	 | ("TCLSOLVE",l) -> tclSOLVE (List.map interp l)
-	 | ("CALL",macro::args) ->
-	     interp (macro_expand loc (nvar_of_ast macro) 
-		       (List.map cvt_arg args))
-	 | _ -> interp_atomic loc opn (List.map cvt_arg tl))
-  | ast -> user_err_loc(Ast.loc ast,"Tacinterp.interp",
-			[< 'sTR"A non-ASTnode constructor was found" >])
-	
-and interp_atomic loc opn args = 
-  try 
-    tacinterp_map opn args
-  with Not_found ->
-    try 
-      vernac_tactic(opn,args)
-    with e -> 
-      Stdpp.raise_with_loc loc e
-	
-and interp_semi_list acc = function
-  | (Node(_,"TACLIST",seq))::l ->
-      interp_semi_list (tclTHENS acc (List.map interp seq)) l
-  | t::l -> interp_semi_list (tclTHEN acc (interp t)) l
-  | [] -> acc
-
-	
 let is_just_undef_macro ast =
   match ast with
     | Node(_,"TACTICLIST",[Node(loc,"CALL",macro::_)]) ->
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 3e913f808a..87d5e2a1ff 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -4,25 +4,42 @@
 (*i*)
 open Pp
 open Names
-open Proof_trees
+open Proof_type
 open Tacmach
 open Term
 (*i*)
 
-(* Interpretation of tactics. *)
+(*Values for interpretation*)
+type value=
+   VTactic of tactic
+  |VFTactic of tactic_arg list*(tactic_arg list->tactic)
+  |VRTactic of (goal list sigma * validation)
+  |VArg of tactic_arg
+  |VFun of (string*value) list*string option list*Coqast.t
+  |VVoid
+  |VRec of value ref;;
 
-val cvt_arg              : Coqast.t -> tactic_arg
+(*Gives the constr corresponding to a CONSTR tactic_arg*)
+val constr_of_Constr:tactic_arg-> constr;;
+
+(*Signature for interpretation: val_interp and interpretation functions*)
+type interp_sign=
+  evar_declarations*Environ.env*(string*value) list*(int*constr) list*
+    goal sigma option;;
+
+(*Adds a Tactic Definition in the table*)
+val add_tacdef : string -> value -> unit;;
+
+(*Interprets any expression*)
+val val_interp:interp_sign->Coqast.t->value;;
+
+(*Interprets tactic arguments*)
+val interp_tacarg:interp_sign->Coqast.t->tactic_arg;;
 
-val tacinterp_add        : string * (tactic_arg list -> tactic) -> unit
-val tacinterp_map        : string -> tactic_arg list -> tactic
-val tacinterp_init       : unit -> unit
 val interp               : Coqast.t -> tactic
-val interp_atomic        : Coqast.loc -> string -> tactic_arg list -> tactic
-val interp_semi_list     : tactic -> Coqast.t list -> tactic
 val vernac_interp        : Coqast.t -> tactic
 val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
-val overwriting_tacinterp_add : string * (tactic_arg list -> tactic) -> unit
+
 val is_just_undef_macro     : Coqast.t -> string option
 
 val bad_tactic_args : string -> 'a
-
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 9191522dc3..5a69ecf577 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -14,24 +14,21 @@ open Evd
 open Typing
 open Tacred
 open Proof_trees
+open Proof_type
 open Logic
 open Refiner
 open Evar_refiner
 
-
-type 'a sigma = 'a Refiner.sigma
-
-type validation = proof_tree list -> proof_tree
-
-type tactic = goal sigma -> (goal list sigma * validation)
-
 let re_sig it gc = { it = it; sigma = gc }
 
-
 (**************************************************************)
 (* Operations for handling terms under a local typing context *)
 (**************************************************************)
 
+type 'a sigma   = 'a Proof_type.sigma;;
+type validation = Proof_type.validation;;
+type tactic     = Proof_type.tactic;;
+
 let unpackage = Refiner.unpackage
 let repackage = Refiner.repackage
 let apply_sig_tac = Refiner.apply_sig_tac
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 9a946e7620..0baa909c99 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -8,6 +8,7 @@ open Sign
 open Environ
 open Reduction
 open Proof_trees
+open Proof_type
 open Refiner
 open Evar_refiner
 open Tacred
@@ -15,7 +16,9 @@ open Tacred
 
 (* Operations for handling terms under a local typing context. *)
 
-type 'a sigma
+type 'a sigma   = 'a Proof_type.sigma;;
+type validation = Proof_type.validation;;
+type tactic     = Proof_type.tactic;;
 
 val sig_it  : 'a sigma   -> 'a
 val sig_sig : goal sigma -> global_constraints
@@ -73,8 +76,6 @@ val pf_const_value : goal sigma -> constr -> constr
 val pf_conv_x      : goal sigma -> constr -> constr -> bool
 val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
-type validation            = proof_tree list -> proof_tree
-type tactic                = goal sigma -> (goal list sigma * validation)
 type transformation_tactic = proof_tree -> (goal list * validation)
 
 val frontier : transformation_tactic