Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

12 files changed, 158 insertions, 217 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index ce56a980d5..44c5aafb08 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -19,11 +19,14 @@ open Instantiate
 open Environ
 open Evd
 open Proof_type
+open Refiner
 open Proof_trees
 open Logic
 open Reductionops
 open Tacmach
 open Evar_refiner
+open Rawterm
+open Tacexpr
 
 (* if lname_typ is [xn,An;..;x1,A1] and l is a list of terms,
    gives [x1:A1]..[xn:An]c' such that c converts to ([x1:A1]..[xn:An]c' l) *)
@@ -48,9 +51,9 @@ let abstract_list_all env sigma typ c l =
     raise (RefinerError (CannotGeneralize typ))
 
 (* Generator of metavariables *)
-let meta_ctr=ref 0;;
+let meta_ctr = ref 0;;
 
-let new_meta ()=incr meta_ctr;!meta_ctr;;
+let new_meta () = incr meta_ctr;!meta_ctr;;
 
 (* replaces a mapping of existentials into a mapping of metas.
    Problem if an evar appears in the type of another one (pops anomaly) *)
@@ -964,23 +967,22 @@ let clenv_match_args s clause =
     | [] -> clause
     | (b,c)::t ->
 	let k =
-	  (match b with
-             | Dep s ->
-		 if List.mem_assoc b t then 
-		   errorlabstrm "clenv_match_args" 
-		     (str "The variable " ++ pr_id s ++ 
-			str " occurs more than once in binding")
-		 else
-		   clenv_lookup_name clause s
-	     | NoDep n ->
-		 if List.mem_assoc b t then errorlabstrm "clenv_match_args"
-		   (str "The position " ++ int n ++
-		      str " occurs more than once in binding");
-		 (try 
-		    List.nth mvs (n-1)
-		  with (Failure _|Invalid_argument _) ->
-                    errorlabstrm "clenv_match_args" (str "No such binder"))
-	     | Com -> anomaly "No free term in clenv_match_args")
+	  match b with
+            | NamedHyp s ->
+		if List.mem_assoc b t then 
+		  errorlabstrm "clenv_match_args" 
+		    (str "The variable " ++ pr_id s ++ 
+		    str " occurs more than once in binding")
+		else
+		  clenv_lookup_name clause s
+	    | AnonHyp n ->
+		if List.mem_assoc b t then errorlabstrm "clenv_match_args"
+		  (str "The position " ++ int n ++
+		  str " occurs more than once in binding");
+		try 
+		  List.nth mvs (n-1)
+		with (Failure _|Invalid_argument _) ->
+                  errorlabstrm "clenv_match_args" (str "No such binder")
 	in
 	let k_typ = w_hnf_constr clause.hook (clenv_instance_type clause k)
 	and c_typ = w_hnf_constr clause.hook (w_type_of clause.hook c) in
@@ -1036,21 +1038,15 @@ let e_res_pf kONT clenv gls =
 
 (* Clausal environment for an application *)
 
-let collect_com lbind = 
-  map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind
-
-let make_clenv_binding_gen n wc (c,t) lbind = 
-  let largs = collect_com lbind in
-  let lcomargs = List.length largs in
-  if lcomargs = List.length lbind then 
-    let clause = mk_clenv_from_n wc n (c,t) in
-    clenv_constrain_dep_args (n <> None) clause largs
-  else if lcomargs = 0 then 
-    let clause = mk_clenv_rename_from_n wc n (c,t) in
-    clenv_match_args lbind clause
-  else 
-    errorlabstrm "make_clenv_bindings"
-      (str "Cannot mix bindings and free associations")
+let make_clenv_binding_gen n wc (c,t) = function
+  | ImplicitBindings largs ->
+      let clause = mk_clenv_from_n wc n (c,t) in
+      clenv_constrain_dep_args (n <> None) clause largs
+  | ExplicitBindings lbind ->
+      let clause = mk_clenv_rename_from_n wc n (c,t) in
+      clenv_match_args lbind clause
+  | NoBindings ->
+      mk_clenv_from_n wc n (c,t)
 
 let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc
 let make_clenv_binding = make_clenv_binding_gen None
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 2033538761..54334c45a0 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -93,15 +93,17 @@ val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
 val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
 *)
 val clenv_lookup_name : 'a clausenv -> identifier -> int
-val clenv_match_args : (bindOcc * constr) list -> wc clausenv -> wc clausenv
+val clenv_match_args : constr Rawterm.explicit_substitution -> wc clausenv -> wc clausenv
 val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
 val clenv_type_of : wc clausenv -> constr -> constr
 val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
 
 val make_clenv_binding_apply :
-  wc -> int -> constr * types -> constr substitution -> wc clausenv
+  named_context sigma -> int -> constr * constr ->
+      types Rawterm.substitution -> named_context sigma clausenv
 val make_clenv_binding :
-  wc -> constr * types -> constr substitution -> wc clausenv
+  named_context sigma -> constr * constr ->
+      types Rawterm.substitution -> named_context sigma clausenv
 
 (* Exported for program.ml only *)
 val clenv_add_sign : 
@@ -110,10 +112,6 @@ val unify_to_subterm :
   wc clausenv -> constr * constr -> wc clausenv * constr
 val unify_to_subterm_list : 
   bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
-(*
-val clenv_constrain_dep_args_of : 
-  int -> constr list -> wc clausenv -> wc clausenv
-*)
 val clenv_typed_unify :
   Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 521cd9b4d7..91e13aeed4 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -23,6 +23,7 @@ open Proof_trees
 open Proof_type
 open Logic
 open Refiner
+open Tacexpr
 
 type wc = named_context sigma (* for a better reading of the following *)
 
@@ -148,12 +149,14 @@ let pfic gls c =
   let evc = gls.sigma in 
   Astterm.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
 
+(*
 let instantiate_tac = function
   | [Integer n; Command com] ->
       (fun gl -> instantiate n (pfic gl com) gl)
   | [Integer n; Constr c] ->
       (fun gl -> instantiate n c gl)
   | _ -> invalid_arg "Instantiate called with bad arguments"
+*)
 
 (* vernac command existential *)
 
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index f791f3abae..46b0db62e5 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -53,5 +53,7 @@ val w_const_value       : wc -> constant -> constr
 val w_defined_evar      : wc -> existential_key -> bool
 
 val instantiate : evar -> constr -> tactic
+(*
 val instantiate_tac : tactic_arg list -> tactic
+*)
 val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
diff --git a/proofs/logic.ml b/proofs/logic.ml
index eb0b94671a..2391ece78a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -43,7 +43,6 @@ type refiner_error =
   (* Errors raised by the tactics *)
   | CannotUnify of constr * constr
   | CannotGeneralize of constr
-  | BadTacticArgs of string * tactic_arg list
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * identifier
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index ba1ca70318..dfe40228f6 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -55,7 +55,6 @@ type refiner_error =
   (*i Errors raised by the tactics i*)
   | CannotUnify of constr * constr
   | CannotGeneralize of constr
-  | BadTacticArgs of string * tactic_arg list
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * identifier
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 035e7af583..410e800935 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -34,7 +34,8 @@ open Safe_typing
 type proof_topstate = {
   top_hyps : named_context * named_context;
   top_goal : goal;
-  top_strength : strength }
+  top_strength : bool * Nametab.strength;
+  top_hook : declaration_hook }
 
 let proof_edits =
   (Edit.empty() : (identifier,pftreestate,proof_topstate) Edit.t)
@@ -105,7 +106,7 @@ let get_current_proof_name () =
     | Some(na,_,_) -> na
 
 let add_proof (na,pfs,ts) =
-  Edit.create proof_edits (na,pfs,ts,Some !undo_limit)
+  Edit.create proof_edits (na,pfs,ts,Some (!undo_limit+1))
     
 let delete_proof na =
   try 
@@ -149,14 +150,16 @@ let subtree_solved () =
 (*********************************************************************)
 (*                 Undo functions                                    *)
 (*********************************************************************)
-    
-let set_undo n = 
-  if n>=0 then 
-    undo_limit := n+1
-  else 
-    error "Cannot set a negative undo limit"
-      
-let reset_undo  () = set_undo undo_default
+
+let set_undo = function
+  | None -> undo_limit := undo_default
+  | Some n -> 
+      if n>=0 then 
+	undo_limit := n
+      else 
+	error "Cannot set a negative undo limit"
+
+let get_undo () = Some !undo_limit
 
 let undo n =
   try 
@@ -182,7 +185,7 @@ let cook_proof () =
    ({ const_entry_body = pfterm;
       const_entry_type = Some concl;
       const_entry_opaque = true },
-    strength))
+    strength, ts.top_hook))
 
 (*********************************************************************)
 (*              Abort   functions                                    *)
@@ -204,12 +207,13 @@ let delete_all_proofs = init_proofs
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof na str sign concl =
+let start_proof na str sign concl hook =
   let top_goal = mk_goal sign concl in
   let ts = { 
     top_hyps = (sign,empty_named_context);
     top_goal = top_goal;
-    top_strength = str }
+    top_strength = str;
+    top_hook = hook}
   in
   start(na,ts);
   set_current_proof na
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 462134fcef..bb828e287c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -14,7 +14,7 @@ open Names
 open Term
 open Sign
 open Environ
-open Declare
+open Nametab
 open Proof_type
 open Tacmach
 (*i*)
@@ -56,18 +56,17 @@ val delete_all_proofs : unit -> unit
 
 val undo : int -> unit
 
-(* [set_undo n] sets the size of the ``undo'' stack *)
+(* [set_undo (Some n)] sets the size of the ``undo'' stack; [set_undo None]
+   sets the size to the default value (12) *)
 
-val set_undo : int -> unit
-
-(* [reset_undo n] sets the size of the ``undo'' stack to the default
-   value (12) *)
-
-val reset_undo : unit -> unit
+val set_undo : int option -> unit
+val get_undo : unit -> int option
 
 (*s [start_proof s str env t] starts a proof of name [s] and conclusion [t] *)
 
-val start_proof : identifier -> strength -> named_context -> constr -> unit
+val start_proof : 
+  identifier -> bool * strength -> named_context -> constr
+    -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
@@ -93,7 +92,9 @@ val suspend_proof : unit -> unit
     into a constant with its name and strength; it fails if there is
     no current proof of if it is not completed *)
 
-val cook_proof : unit -> identifier * (Safe_typing.constant_entry * strength)
+val cook_proof : unit -> 
+  identifier *
+  (Safe_typing.constant_entry * (bool * strength) * declaration_hook)
 
 (*s [get_pftreestate ()] returns the current focused pending proof or
    raises [UserError "no focused proof"] *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 115367cd79..7777f34638 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -24,6 +24,7 @@ open Proof_trees
 open Proof_type
 open Logic
 open Refiner
+open Tacexpr
 
 let re_sig it gc = { it = it; sigma = gc }
 
@@ -164,40 +165,6 @@ let top_of_tree             = top_of_tree
 let frontier                = frontier
 let change_constraints_pftreestate = change_constraints_pftreestate
 
-(*************************************************)
-(* Tacticals re-exported from the Refiner module.*)
-(*************************************************)
-
-(* A special exception for levels for the Fail tactic *)
-exception FailError = Refiner.FailError
-
-let tclIDTAC         = tclIDTAC
-let tclORELSE        = tclORELSE
-let tclTHEN          = tclTHEN
-let tclTHENLIST      = tclTHENLIST
-let tclTHEN_i        = tclTHEN_i
-let tclTHENL         = tclTHENL
-let tclTHENS         = tclTHENS
-let tclTHENSi        = tclTHENSi
-let tclTHENST        = tclTHENST
-let tclTHENSI        = tclTHENSI
-let tclREPEAT        = tclREPEAT
-let tclREPEAT_MAIN   = tclREPEAT_MAIN
-let tclFIRST         = tclFIRST
-let tclSOLVE         = tclSOLVE
-let tclTRY           = tclTRY
-let tclTHENTRY       = tclTHENTRY
-let tclCOMPLETE      = tclCOMPLETE
-let tclAT_LEAST_ONCE = tclAT_LEAST_ONCE
-let tclFAIL          = tclFAIL
-let tclDO            = tclDO
-let tclPROGRESS      = tclPROGRESS
-let tclWEAK_PROGRESS = tclWEAK_PROGRESS
-let tclNOTSAMEGOAL   = tclNOTSAMEGOAL
-let tclINFO          = tclINFO
-
-let unTAC            = unTAC
-
 
 (********************************************)
 (* Definition of the most primitive tactics *)
@@ -258,11 +225,13 @@ let rename_bound_var_goal gls =
 (* The interpreter of defined tactics *)
 (***************************************)
 
+(*
 let vernac_tactic = vernac_tactic
 
 let add_tactic = Refiner.add_tactic
 
 let overwriting_tactic = Refiner.overwriting_add_tactic
+*)
 
 
 (* Some combinators for parsing tactic arguments. 
@@ -302,26 +271,38 @@ let tactic_com_list =
     let translate = pf_interp_constr x in 
     tac (List.map translate tl) x
 
+open Rawterm 
+
 let tactic_bind_list =
   fun tac tl x -> 
     let translate = pf_interp_constr x in 
-    tac (List.map (fun (b,c)->(b,translate c)) tl) x
+    let tl =
+    match tl with
+      | NoBindings -> NoBindings
+      | ImplicitBindings l -> ImplicitBindings (List.map translate l)
+      | ExplicitBindings l ->
+	  ExplicitBindings (List.map (fun (b,c)->(b,translate c)) l)
+    in tac tl x
+
+let translate_bindings gl = function
+  | NoBindings -> NoBindings
+  | ImplicitBindings l -> ImplicitBindings (List.map (pf_interp_constr gl) l)
+  | ExplicitBindings l ->
+      ExplicitBindings (List.map (fun (b,c)->(b,pf_interp_constr gl c)) l)
 
 let tactic_com_bind_list =
-  fun tac (c,tl) x -> 
-    let translate = pf_interp_constr x in 
-    tac (translate c,List.map (fun (b,c')->(b,translate c')) tl) x
+  fun tac (c,tl) gl -> 
+    let translate = pf_interp_constr gl in 
+    tac (translate c,translate_bindings gl tl) gl
 
 let tactic_com_bind_list_list =
   fun tac args gl -> 
-    let translate (c,tl) = 
-      (pf_interp_constr gl c,
-       List.map (fun (b,c')->(b,pf_interp_constr gl c')) tl)
+    let translate (c,tl) = (pf_interp_constr gl c, translate_bindings gl tl)
     in 
     tac (List.map translate args) gl
 
 (* Some useful combinators for hiding tactic implementations *)
-
+(*
 type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic)
 
 let hide_atomic_tactic s tac = 
@@ -331,45 +312,48 @@ let hide_atomic_tactic s tac =
 let overwrite_hidden_atomic_tactic s tac =
   overwriting_tactic s (function [] -> tac | _ -> assert false);
   vernac_tactic(s,[])
-
-
+*)
+(*
 let hide_constr_comarg_tactic s tac =
   let tacfun = function 
     | [Constr c]    -> tac c
-    | [Command com] -> tactic_com tac com
-    | _ -> anomaly "hide_constr_comarg_tactic : neither CONSTR nor COMMAND"
+(*    | [Command com] -> tactic_com tac com*)
+    | _ -> anomaly "hide_constr_comarg_tactic : neither CONSTR nor CONSTR"
   in 
   add_tactic s tacfun;
   (fun c -> vernac_tactic(s,[Constr c]),
-   fun com -> vernac_tactic(s,[Command com]))
- 
+   (* fun com -> vernac_tactic(s,[Command com]) *) fun _ -> failwith "Command unsupported")
+*)
+(* 
 let overwrite_hidden_constr_comarg_tactic s tac =
   let tacfun = function 
     | [Constr c] -> tac c
-    | [Command com] -> 
-        (fun gls -> tac (pf_interp_constr gls com) gls)
+(*    | [Command com] -> 
+        (fun gls -> tac (pf_interp_constr gls com) gls)*)
     | _ -> 
 	anomaly 
-	  "overwrite_hidden_constr_comarg_tactic : neither CONSTR nor COMMAND"
+	  "overwrite_hidden_constr_comarg_tactic : neither CONSTR nor CONSTR"
   in 
   overwriting_tactic s tacfun;
   (fun c -> vernac_tactic(s,[(Constr c)]), 
-   fun c -> vernac_tactic(s,[(Command c)]))
-
+   (*fun c -> vernac_tactic(s,[(Command c)])*) fun _ -> failwith "Command unsupported")
+*)
+(*
 let hide_constr_tactic s tac =
   let tacfun = function 
     | [Constr c]    -> tac c
-    | [Command com] -> tactic_com tac com
-    | _ -> anomaly "hide_constr_tactic : neither CONSTR nor COMMAND"
+(*    | [Command com] -> tactic_com tac com*)
+    | _ -> anomaly "hide_constr_tactic : neither CONSTR nor CONSTR"
   in 
   add_tactic s tacfun;
   (fun c  -> vernac_tactic(s,[(Constr c)]))
-
+*)
+(*
 let hide_openconstr_tactic s tac =
   let tacfun = function 
     | [OpenConstr c] -> tac c
-    | [Command com] -> tactic_opencom tac com
-    | _ -> anomaly "hide_openconstr_tactic : neither OPENCONSTR nor COMMAND"
+(*    | [Command com] -> tactic_opencom tac com*)
+    | _ -> anomaly "hide_openconstr_tactic : neither OPENCONSTR nor CONSTR"
   in 
   add_tactic s tacfun;
   (fun c  -> vernac_tactic(s,[(OpenConstr c)]))
@@ -393,40 +377,44 @@ let hide_identl_tactic s tac =
   let tacfun = (function [Clause idl] -> tac idl | _ -> assert false) in 
   add_tactic s tacfun;
   fun idl -> vernac_tactic(s,[Clause idl])
-
+*)
+(*
 let hide_constrl_tactic s tac = 
   let tacfun = function 
-    | ((Command com)::_) as al -> 
+(*    | ((Command com)::_) as al -> 
       	tactic_com_list tac 
-          (List.map (function (Command com) -> com | _ -> assert false) al)
+          (List.map (function (Command com) -> com | _ -> assert false) al)*)
     | ((Constr com)::_) as al ->
       	tac (List.map (function (Constr c) -> c | _ -> assert false) al)
-    | _ -> anomaly "hide_constrl_tactic : neither CONSTR nor COMMAND"
+    | _ -> anomaly "hide_constrl_tactic : neither CONSTR nor CONSTR"
   in 
   add_tactic s tacfun;
   fun ids -> vernac_tactic(s,(List.map (fun id -> Constr id) ids))
-
+*)
+(*
 let hide_bindl_tactic s tac = 
   let tacfun = function  
-    | [Bindings  al] -> tactic_bind_list tac al
+(*    | [Bindings  al] -> tactic_bind_list tac al*)
     | [Cbindings al] -> tac al
     | _ -> anomaly "hide_bindl_tactic : neither BINDINGS nor CBINDINGS"
   in 
   add_tactic s tacfun;
   fun bindl -> vernac_tactic(s,[Cbindings bindl])
-      
+*)    
+(*
 let hide_cbindl_tactic s tac = 
   let tacfun = function 
-    | [Command com; Bindings al] -> tactic_com_bind_list tac (com,al)
+(*    | [Command com; Bindings al] -> tactic_com_bind_list tac (com,al)*)
     | [Constr c; Cbindings al]  -> tac (c,al)
-    | _ -> anomaly "hide_cbindl_tactic : neither CONSTR nor COMMAND"
+    | _ -> anomaly "hide_cbindl_tactic : neither CONSTR nor CONSTR"
   in 
   add_tactic s tacfun;
   fun (c,bindl) -> vernac_tactic(s,[Constr c; Cbindings bindl])
-      
+*)
+(*      
 let hide_cbindll_tactic s tac = 
   let rec getcombinds = function 
-    | ((Command com)::(Bindings al)::l) -> (com,al)::(getcombinds l)
+(*    | ((Command com)::(Bindings al)::l) -> (com,al)::(getcombinds l)*)
     | []                                ->  [] 
     | _ -> anomaly "hide_cbindll_tactic : not the expected form" 
   in  
@@ -440,19 +428,21 @@ let hide_cbindll_tactic s tac =
     |  []          -> [] 
   in
   let tacfun = function 
-    | ((Command com)::_) as args -> 
-      	tactic_com_bind_list_list tac (getcombinds args)
+(*    | ((Command com)::_) as args -> 
+      	tactic_com_bind_list_list tac (getcombinds args)*)
     | ((Constr com)::_) as args -> tac (getconstrbinds args)
-    | _ -> anomaly "hide_cbindll_tactic : neither CONSTR nor COMMAND"
+    | _ -> anomaly "hide_cbindll_tactic : neither CONSTR nor CONSTR"
   in 
   add_tactic s tacfun;
   fun l -> vernac_tactic(s,putconstrbinds l)
-
+*)
 
 (* Pretty-printers *)
 
 open Pp
 open Printer
+open Tacexpr
+open Rawterm
 
 let pr_com sigma goal com =
   prterm (rename_bound_var (Global.env())
@@ -460,15 +450,17 @@ let pr_com sigma goal com =
             (Astterm.interp_constr sigma (Evarutil.evar_env goal) com))
 
 let pr_one_binding sigma goal = function
-  | (Dep id,com)  -> pr_id id ++ str ":=" ++ pr_com sigma goal com
-  | (NoDep n,com) -> int n  ++ str ":=" ++ pr_com sigma goal com
-  | (Com,com)     -> pr_com sigma goal com
+  | (NamedHyp id,com) -> pr_id id ++ str ":=" ++ pr_com sigma goal com
+  | (AnonHyp n,com) -> int n  ++ str ":=" ++ pr_com sigma goal com
 
 let pr_bindings sigma goal lb =
   let prf = pr_one_binding sigma goal in
   match lb with 
-    | [] -> prlist_with_sep pr_spc prf lb
-    | _  -> str "with" ++ spc () ++ prlist_with_sep pr_spc prf lb
+    | ImplicitBindings l ->
+	str "with" ++ spc () ++ prlist_with_sep pr_spc (pr_com sigma goal) l
+    | ExplicitBindings l ->
+	str "with" ++ spc () ++ prlist_with_sep pr_spc prf l
+    | NoBindings -> mt ()
 	  
 let rec pr_list f = function
   | []   -> mt ()
@@ -480,5 +472,4 @@ let pr_gls gls =
 let pr_glls glls =
   hov 0 (pr_decls (sig_sig glls) ++ fnl () ++
          prlist_with_sep pr_fnl pr_seq (sig_it glls))
-    
-let pr_tactic = Refiner.pr_tactic
+  
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index ee09b7ada5..49a2db4197 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -19,6 +19,8 @@ open Proof_trees
 open Proof_type
 open Refiner
 open Tacred
+open Tacexpr
+open Rawterm
 (*i*)
 
 (* Operations for handling terms under a local typing context. *)
@@ -115,39 +117,9 @@ val top_of_tree             : pftreestate -> pftreestate
 val change_constraints_pftreestate :
   evar_map -> pftreestate -> pftreestate
 
-(*s Tacticals re-exported from the Refiner module. *)
-
-(* A special exception for levels for the Fail tactic *)
-exception FailError of int
-
-val tclIDTAC         : tactic
-val tclORELSE        : tactic -> tactic -> tactic
-val tclTHEN          : tactic -> tactic -> tactic
-val tclTHENLIST      : tactic list -> tactic
-val tclTHEN_i        : tactic -> (int -> tactic) -> tactic
-val tclTHENL         : tactic -> tactic -> tactic
-val tclTHENS         : tactic -> tactic list -> tactic
-val tclTHENSi        : tactic -> tactic list -> (int -> tactic) -> tactic
-val tclTHENST        : tactic -> tactic list -> tactic -> tactic
-val tclTHENSI        : tactic -> tactic list -> tactic
-val tclREPEAT        : tactic -> tactic
-val tclREPEAT_MAIN   : tactic -> tactic
-val tclFIRST         : tactic list -> tactic
-val tclSOLVE         : tactic list -> tactic
-val tclTRY           : tactic -> tactic
-val tclTHENTRY       : tactic -> tactic -> tactic
-val tclCOMPLETE      : tactic -> tactic
-val tclAT_LEAST_ONCE : tactic -> tactic
-val tclFAIL          : int -> tactic
-val tclDO            : int -> tactic -> tactic
-val tclPROGRESS      : tactic -> tactic
-val tclWEAK_PROGRESS : tactic -> tactic
-val tclNOTSAMEGOAL   : tactic -> tactic
-val tclINFO          : tactic -> tactic
-
-val unTAC         : tactic -> goal sigma -> proof_tree sigma
-val vernac_tactic : tactic_expression -> tactic
-
+(*
+val vernac_tactic : string * tactic_arg list -> tactic
+*)
 (*s The most primitive tactics. *)
 
 val refiner         : rule -> tactic
@@ -185,9 +157,10 @@ val tclIDTAC_list      : tactic_list
 
 (*s Tactic Registration. *)
 
+(*
 val add_tactic         : string -> (tactic_arg list -> tactic) -> unit
 val overwriting_tactic : string -> (tactic_arg list -> tactic) -> unit
-
+*)
 
 (*s Transformation of tactic arguments. *)
 
@@ -197,42 +170,16 @@ val tactic_com       : (constr,Coqast.t) parse_combinator
 val tactic_com_sort  : (constr,Coqast.t) parse_combinator
 val tactic_com_list  : (constr list, Coqast.t list) parse_combinator
 
-val tactic_bind_list : ((bindOcc * constr) list,
-                        (bindOcc * Coqast.t) list) parse_combinator
+val tactic_bind_list :
+  (constr substitution, Coqast.t substitution) parse_combinator
 
 val tactic_com_bind_list : 
-  (constr   * (bindOcc * constr)   list,
-   Coqast.t * (bindOcc * Coqast.t) list) parse_combinator
+  (constr   * constr substitution,
+   Coqast.t * Coqast.t substitution) parse_combinator
 
 val tactic_com_bind_list_list :  
-  ((constr   * (bindOcc * constr)   list) list, 
-   (Coqast.t * (bindOcc * Coqast.t) list) list) parse_combinator
-
-
-(*s Hiding the implementation of tactics. *)
-
-val hide_tactic  : 
-  string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
-
-val overwrite_hidden_tactic : 
-  string -> (tactic_arg list -> tactic) -> (tactic_arg list -> tactic)
-
-
-type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic)
-
-val hide_atomic_tactic  : string -> tactic -> tactic
-val hide_constr_tactic  : constr hide_combinator
-val hide_openconstr_tactic  : Pretyping.open_constr hide_combinator
-val hide_constrl_tactic : (constr list) hide_combinator
-val hide_numarg_tactic  : int hide_combinator
-val hide_ident_tactic   : identifier hide_combinator
-val hide_identl_tactic  : hyp_location list hide_combinator
-val hide_string_tactic  : string hide_combinator
-val hide_bindl_tactic   : ((bindOcc * constr) list) hide_combinator
-val hide_cbindl_tactic  : (constr * (bindOcc * constr) list) hide_combinator
-val hide_cbindll_tactic : 
-  ((constr * (bindOcc * constr) list) list) hide_combinator
-
+  ((constr   * constr substitution) list, 
+   (Coqast.t * Coqast.t substitution) list) parse_combinator
 
 (*s Pretty-printing functions. *)
 
@@ -243,4 +190,3 @@ open Pp
 val pr_com    : evar_map -> goal -> Coqast.t -> std_ppcmds
 val pr_gls    : goal sigma -> std_ppcmds
 val pr_glls   : goal list sigma -> std_ppcmds
-val pr_tactic : tactic_expression -> std_ppcmds
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 61ccbcac7c..43162f05d4 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -7,6 +7,7 @@
 (***********************************************************************)
 open Ast
 open Pp
+open Pptactic
 open Printer
 
 (* This module intends to be a beginning of debugger for tactic expressions.
@@ -33,7 +34,7 @@ let help () =
 (* Prints the state and waits for an instruction *)
 let debug_prompt goalopt tac_ast =
   db_pr_goal goalopt;
-  msg (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl ());
+  msg (str "Going to execute:" ++ fnl () ++ (pr_raw_tactic tac_ast) ++ fnl ());
 (*         str "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*)
 (*  mSG (str "Going to execute:" ++ fnl () ++ (gentacpr tac_ast) ++ fnl () ++ fnl () ++
          str "----<Enter>=Continue----s=Skip----x=Exit----");*)
@@ -62,7 +63,7 @@ let db_constr debug env c =
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,c) =
   if debug = DebugOn then
-    msgnl (str "Matched hypothesis --> " ++ str (id^": ") ++
+    msgnl (str "Matched hypothesis --> " ++ str (Names.string_of_id id^": ") ++
            prterm_env env c)
 
 (* Prints the matched conclusion *)
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 4a6aecfde9..b05a33fdfc 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 open Proof_type
+open Names
 open Term
 
 (* This module intends to be a beginning of debugger for tactic expressions.
@@ -22,13 +23,13 @@ type debug_info =
   | Exit
 
 (* Prints the state and waits *)
-val debug_prompt : goal sigma option -> Coqast.t -> debug_info
+val debug_prompt : goal sigma option -> Tacexpr.raw_tactic_expr -> debug_info
 
 (* Prints a constr *)
 val db_constr : debug_info -> Environ.env -> constr -> unit
 
 (* Prints a matched hypothesis *)
-val db_matched_hyp : debug_info -> Environ.env -> string * constr -> unit
+val db_matched_hyp : debug_info -> Environ.env -> identifier * constr -> unit
 
 (* Prints the matched conclusion *)
 val db_matched_concl : debug_info -> Environ.env -> constr -> unit