Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

11 files changed, 67 insertions, 427 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 91e13aeed4..09879d5852 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -147,7 +147,7 @@ let instantiate n c gl =
 
 let pfic gls c =
   let evc = gls.sigma in 
-  Astterm.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
+  Constrintern.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
 
 (*
 let instantiate_tac = function
@@ -170,7 +170,7 @@ let instantiate_pf_com n com pfts =
     with Failure _ -> 
       error "not so many uninstantiated existential variables"
   in 
-  let c = Astterm.interp_constr sigma (Evarutil.evar_env evd) com in     
+  let c = Constrintern.interp_constr sigma (Evarutil.evar_env evd) com in     
   let wc' = w_Define sp c wc in
   let newgc = (w_Underlying wc') in
   change_constraints_pftreestate newgc pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 46b0db62e5..b0dd5e4f45 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -56,4 +56,4 @@ val instantiate : evar -> constr -> tactic
 (*
 val instantiate_tac : tactic_arg list -> tactic
 *)
-val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
+val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 9e0bcf178e..6f682f1133 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -22,9 +22,9 @@ open Declare
 open Typing
 open Tacmach
 open Proof_trees
+open Tacexpr
 open Proof_type
 open Lib
-open Astterm
 open Safe_typing
 
 (*********************************************************************)
@@ -76,14 +76,13 @@ let get_goal_context n =
 
 let get_current_goal_context () = get_goal_context 1
 
-let set_current_proof s = 
+let set_current_proof = Edit.focus proof_edits
+
+let resume_proof (loc,id) = 
   try 
-    Edit.focus proof_edits s
+    Edit.focus proof_edits id
   with Invalid_argument "Edit.focus" ->
-    errorlabstrm "Pfedit.set_proof"
-      (str"No such proof" ++ (msg_proofs false))
-
-let resume_proof = set_current_proof
+    user_err_loc(loc,"Pfedit.set_proof",str"No such proof" ++ msg_proofs false)
 
 let suspend_proof () =
   try 
@@ -108,13 +107,15 @@ let get_current_proof_name () =
 
 let add_proof (na,pfs,ts) =
   Edit.create proof_edits (na,pfs,ts,Some (!undo_limit+1))
-    
-let delete_proof na =
+
+let delete_proof_gen = Edit.delete proof_edits
+
+let delete_proof (loc,id) =
   try 
-    Edit.delete proof_edits na
+    delete_proof_gen id
   with (UserError ("Edit.delete",_)) ->
-    errorlabstrm "Pfedit.delete_proof"
-      (str"No such proof" ++ msg_proofs false)
+    user_err_loc
+      (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
       
 let init_proofs () = Edit.clear proof_edits
 		       
@@ -135,7 +136,7 @@ let restart_proof () =
 	errorlabstrm "Pfedit.restart"
           (str"No focused proof to restart" ++ msg_proofs true)
     | Some(na,_,ts) -> 
-	delete_proof na;
+	delete_proof_gen na;
         start (na,ts);
         set_current_proof na
 
@@ -204,7 +205,7 @@ let check_no_pending_proofs () =
       (str"Proof editing in progress" ++ (msg_proofs false) ++
          str"Use \"Abort All\" first or complete proof(s).")
 
-let delete_current_proof () = delete_proof (get_current_proof_name ())
+let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
 
 let delete_all_proofs = init_proofs
    
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index dd3ac60337..8cf1cffe11 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -9,14 +9,15 @@
 (*i $Id$ i*)
 
 (*i*)
+open Util
 open Pp
 open Names
 open Term
 open Sign
 open Environ
 open Decl_kinds
-open Proof_type
 open Tacmach
+open Tacexpr
 (*i*)
 
 (*s Several proofs can be opened simultaneously but at most one is
@@ -39,7 +40,7 @@ val check_no_pending_proofs : unit -> unit
 (*s [delete_proof name] deletes proof of name [name] or fails if no proof
     has this name *)
 
-val delete_proof : identifier -> unit
+val delete_proof : identifier located -> unit
 
 (* [delete_current_proof ()] deletes current focused proof or fails if
     no proof is focused *)
@@ -83,7 +84,7 @@ val resume_last_proof : unit -> unit
 (* [resume_proof name] focuses on the proof of name [name] or
    raises [UserError] if no proof has name [name] *)
 
-val resume_proof : identifier -> unit
+val resume_proof : identifier located -> unit
 
 (* [suspend_proof ()] unfocuses the current focused proof or
    failed with [UserError] if no proof is currently focused *)
@@ -141,7 +142,7 @@ val by : tactic -> unit
    UserError if no proof is focused or if there is no such [n]th
    existential variable *)
 
-val instantiate_nth_evar_com : int -> Coqast.t -> unit
+val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
 
 (*s To deal with subgoal focus *)
 
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 86ec64c76d..34e9a06e78 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -248,122 +248,3 @@ let pr_subgoals_existential sigma = function
       let prest = pr_rec 2 rest in
       v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () 
 	   ++ pg1 ++ prest ++ fnl ())
-
-(*
-open Ast
-open Termast
-open Tacexpr
-open Rawterm
-
-let ast_of_cvt_bind f = function
-  | (NoDepBinding n,c) -> ope ("BINDING", [(num n); ope ("CONSTR",[(f c)])])
-  | (DepBinding  id,c) -> ope ("BINDING", [nvar id; ope  ("CONSTR",[(f c)])]) 
-  | (AnonymousBinding,c) -> ope ("BINDING", [ope ("CONSTR",[(f c)])])
-
-let rec ast_of_cvt_intro_pattern = function
-  | WildPat   -> ope ("WILDCAR",[])
-  | IdPat id  -> nvar id
-(*  | DisjPat l -> ope ("DISJPATTERN",  (List.map ast_of_cvt_intro_pattern l))*)
-  | ConjPat l -> ope ("CONJPATTERN",  (List.map ast_of_cvt_intro_pattern l))
-*)
-(*
-(* Gives the ast list corresponding to a reduction flag *)
-open RedFlags
-
-let last_of_cvt_flags red =
-  (if (red_set red fBETA) then [ope("Beta",[])]
-   else [])@
-  (let (n_unf,lconst) = red_get_const red in
-   let lqid =
-     List.map
-       (function
-	  | EvalVarRef id -> nvar id
-	  | EvalConstRef kn ->
-	      ast_of_qualid
-                (shortest_qualid_of_global None (ConstRef kn)))
-       lconst in
-   if lqid = [] then []
-   else if n_unf then [ope("Delta",[]);ope("UnfBut",lqid)]
-   else [ope("Delta",[]);ope("Unf",lqid)])@
-  (if (red_set red fIOTA) then [ope("Iota",[])]
-   else [])
-*)
-(*
-(* Gives the ast corresponding to a reduction expression *)
-open Rawterm
-
-let ast_of_cvt_redexp = function
-  | Red _ -> ope ("Red",[])
-  | Hnf -> ope("Hnf",[])
-  | Simpl -> ope("Simpl",[])
-(*
-  | Cbv flg -> ope("Cbv",last_of_cvt_flags flg)
-  | Lazy flg -> ope("Lazy",last_of_cvt_flags flg)
-*)
-  | Unfold l ->
-    ope("Unfold",List.map (fun (locc,sp) -> ope("UNFOLD",
-      [match sp with
-	| EvalVarRef id -> nvar id
-	| EvalConstRef kn -> 					
-	    ast_of_qualid
-	      (shortest_qualid_of_global None (ConstRef kn))]
-      @(List.map num locc))) l)
-  | Fold l ->
-    ope("Fold",List.map (fun c -> ope ("CONSTR",
-      [ast_of_constr false (Global.env ()) c])) l)
-  | Pattern l ->
-    ope("Pattern",List.map (fun (locc,csr) -> ope("PATTERN",
-      [ope ("CONSTR",[ast_of_constr false (Global.env ()) csr])]@
-      (List.map num locc))) l)
-*)
-(* Gives the ast corresponding to a tactic argument *)
-(*
-let ast_of_cvt_arg = function
-  | Identifier id   -> nvar id
-(*
-  | Qualid qid      -> ast_of_qualid qid
-*)
-  | Quoted_string s -> string s
-  | Integer n       -> num n 
-(*  | Command c       -> ope ("CONSTR",[c])*)
-  | Constr  c       -> 
-    ope ("CONSTR",[ast_of_constr false (Global.env ()) c])
-  | OpenConstr  (_,c)       -> 
-    ope ("CONSTR",[ast_of_constr false (Global.env ()) c])
-  | Constr_context _ ->
-    anomalylabstrm "ast_of_cvt_arg" (str
-      "Constr_context argument could not be used")
-  | Clause idl      -> 
-      let transl = function
-	| InHyp id -> ope ("INHYP", [nvar id])
-	| InHypType id -> ope ("INHYPTYPE", [nvar id]) in
-      ope ("CLAUSE", List.map transl idl)
-(*
-  | Bindings bl     -> ope ("BINDINGS", 
-			    List.map (ast_of_cvt_bind (fun x -> x)) bl)
-  | Cbindings bl    -> 
-      ope ("BINDINGS", 
-	   List.map 
-	     (ast_of_cvt_bind
-		(ast_of_constr false (Global.env ()))) bl)
-*)
-(* TODO
-  | Tacexp ast      -> ope ("TACTIC",[ast])
-  | Tac (tac,ast) -> ast
-*)
-  | Redexp red -> ope("REDEXP",[ast_of_cvt_redexp red])
-  | Fixexp (id,n,c) -> ope ("FIXEXP",[nvar id; num n; ope ("CONSTR",[ast_of_constr false (Global.env ()) c])])
-  | Cofixexp (id,c) -> ope ("COFIXEXP",[nvar id; ope ("CONSTR",[ast_of_constr false (Global.env ()) c])])
-(*  | Intropattern p ->  ast_of_cvt_intro_pattern p*)
-  | Letpatterns (gl_occ_opt,hyp_occ_list) ->
-     let hyps_pats =
-       List.map
-	 (fun (id,l) ->
-	    ope ("HYPPATTERN", nvar id :: (List.map num l)))
-	 hyp_occ_list in
-     let all_pats =
-       match gl_occ_opt with
-	 | None -> hyps_pats
-	 | Some l -> hyps_pats @ [ope ("CCLPATTERN", List.map num l)] in
-     ope ("LETPATTERNS", all_pats)
-*)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index e3d52c5b36..405d5e5da0 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -71,21 +71,21 @@ and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
   (constr,
-   Closure.evaluable_global_reference,
+   evaluable_global_reference,
    inductive or_metanum,
    identifier)
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
   (constr,
-   Closure.evaluable_global_reference,
+   evaluable_global_reference,
    inductive or_metanum,
    identifier)
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
   (constr,
-   Closure.evaluable_global_reference,
+   evaluable_global_reference,
    inductive or_metanum,
    identifier)
      Tacexpr.gen_tactic_arg
@@ -99,5 +99,3 @@ type closed_generic_argument =
 
 type 'a closed_abstract_argument_type =
     ('a,constr,raw_tactic_expr) abstract_argument_type
-
-type declaration_hook = Decl_kinds.strength -> global_reference -> unit
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 95bf5d3a21..69aa0aff06 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -99,21 +99,21 @@ and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
   (constr,
-   Closure.evaluable_global_reference,
+   evaluable_global_reference,
    inductive or_metanum,
    identifier)
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
   (constr,
-   Closure.evaluable_global_reference,
+   evaluable_global_reference,
    inductive or_metanum,
    identifier)
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
   (constr,
-   Closure.evaluable_global_reference,
+   evaluable_global_reference,
    inductive or_metanum,
    identifier)
      Tacexpr.gen_tactic_arg
@@ -127,5 +127,3 @@ type closed_generic_argument =
 
 type 'a closed_abstract_argument_type =
     ('a,constr,raw_tactic_expr) abstract_argument_type
-
-type declaration_hook = Decl_kinds.strength -> global_reference -> unit
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 16b13ac9ea..a6edd9a3ad 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -212,7 +212,7 @@ let vernac_tactic (s,args) =
 let abstract_tactic te = abstract_tactic_expr (Tacexpr.TacAtom (dummy_loc,te))
 
 let abstract_extended_tactic s args = 
-  abstract_tactic (Tacexpr.TacExtend (s, args))
+  abstract_tactic (Tacexpr.TacExtend (dummy_loc, s, args))
 
 let vernac_tactic (s,args) =
   let tacfun = lookup_tactic s args in
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index a1d7ff16b7..521a08bc2b 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -9,7 +9,7 @@
 (* $Id$ *)
 
 open Names
-open Coqast
+open Topconstr
 open Libnames
 open Nametab
 open Rawterm
@@ -24,10 +24,10 @@ type raw_red_flag =
   | FBeta
   | FIota
   | FZeta
-  | FConst of qualid or_metanum list
-  | FDeltaBut of qualid or_metanum list
+  | FConst of reference or_metanum list
+  | FDeltaBut of reference or_metanum list
 
-type raw_red_expr = (constr_ast, qualid or_metanum) red_expr_gen
+type raw_red_expr = (constr_expr, reference or_metanum) red_expr_gen
 
 let make_red_flag =
   let rec add_flag red = function
@@ -55,10 +55,6 @@ type 'a raw_hyp_location = (* To distinguish body and type of local defs *)
   | InHyp of 'a
   | InHypType of 'a
 
-type extend_tactic_arg =
-  | TacticArgMeta of loc * string
-  | TacticArgAst of Coqast.t
-
 type 'a induction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of identifier located
@@ -73,7 +69,7 @@ type 'id clause_pattern = int list option * ('id * int list) list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
 
-type pattern_ast = Coqast.t
+type pattern_expr = constr_expr
 
 (* Type of patterns *)
 type 'a match_pattern =
@@ -138,7 +134,7 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
   | TacAutoTDB of int option
   | TacDestructHyp of (bool * identifier located)
   | TacDestructConcl
-  | TacSuperAuto of (int option * qualid located list * bool * bool)
+  | TacSuperAuto of (int option * reference list * bool * bool)
   | TacDAuto of int option * int option
 
   (* Context management *)
@@ -164,15 +160,15 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr 
 
   (* For ML extensions *)
-  | TacExtend of string * ('constr,raw_tactic_expr) generic_argument list
+  | TacExtend of loc * string * ('constr,raw_tactic_expr) generic_argument list
 
   (* For syntax extensions *)
   | TacAlias of string *
-      (string * ('constr,raw_tactic_expr) generic_argument) list
+      (identifier * ('constr,raw_tactic_expr) generic_argument) list
       * raw_tactic_expr
 
 and raw_tactic_expr =
-    (constr_ast,qualid or_metanum,qualid or_metanum,identifier located or_metaid) gen_tactic_expr
+    (constr_expr,reference or_metanum,reference or_metanum,identifier located or_metaid) gen_tactic_expr
 
 and ('constr,'cst,'ind,'id) gen_tactic_expr =
   | TacAtom of loc * ('constr,'cst,'ind,'id) gen_atomic_tactic_expr
@@ -191,10 +187,10 @@ and ('constr,'cst,'ind,'id) gen_tactic_expr =
   | TacInfo of ('constr,'cst,'ind,'id) gen_tactic_expr
 
   | TacLetRecIn of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast) list * ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacLetIn of (identifier located * constr_ast may_eval option * ('constr,'cst,'ind,'id) gen_tactic_arg) list * ('constr,'cst,'ind,'id) gen_tactic_expr
-  | TacLetCut of (identifier * constr_ast may_eval * ('constr,'cst,'ind,'id) gen_tactic_arg) list
-  | TacMatch of constr_ast may_eval * (pattern_ast,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
-  | TacMatchContext of direction_flag * (pattern_ast,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
+  | TacLetIn of (identifier located * constr_expr may_eval option * ('constr,'cst,'ind,'id) gen_tactic_arg) list * ('constr,'cst,'ind,'id) gen_tactic_expr
+  | TacLetCut of (identifier * constr_expr may_eval * ('constr,'cst,'ind,'id) gen_tactic_arg) list
+  | TacMatch of constr_expr may_eval * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
+  | TacMatchContext of direction_flag * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'cst,'ind,'id) gen_tactic_fun_ast
   | TacFunRec of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast)
   | TacArg of ('constr,'cst,'ind,'id) gen_tactic_arg
@@ -209,23 +205,32 @@ and ('constr,'cst,'ind,'id) gen_tactic_arg =
   | MetaNumArg     of loc * int
   | MetaIdArg      of loc * string
   | ConstrMayEval  of 'constr may_eval
-  | Reference      of reference_expr
+  | Reference      of reference
   | Integer        of int
   | TacCall        of loc *
-      reference_expr * ('constr,'cst,'ind,'id) gen_tactic_arg list
+      reference * ('constr,'cst,'ind,'id) gen_tactic_arg list
   | Tacexp of raw_tactic_expr
 
 type raw_atomic_tactic_expr =
-    (constr_ast,qualid or_metanum,qualid or_metanum,identifier located or_metaid) gen_atomic_tactic_expr
+    (constr_expr,                 (* constr *)
+     reference or_metanum,        (* evaluable reference *)
+     reference or_metanum,        (* inductive *)
+     identifier located or_metaid (* identifier *)
+    ) gen_atomic_tactic_expr
 
 type raw_tactic_arg =
-    (constr_ast,qualid or_metanum,qualid or_metanum,identifier located or_metaid) gen_tactic_arg
+    (constr_expr,
+     reference or_metanum,
+     reference or_metanum,
+     identifier located or_metaid) gen_tactic_arg
 
 type raw_generic_argument =
-    (constr_ast,raw_tactic_expr) generic_argument
+    (constr_expr,raw_tactic_expr) generic_argument
 
 type closed_raw_generic_argument =
-    (constr_ast,raw_tactic_expr) generic_argument
+    (constr_expr,raw_tactic_expr) generic_argument
 
 type 'a raw_abstract_argument_type =
-    ('a, constr_ast,raw_tactic_expr) abstract_argument_type
+    ('a, constr_expr,raw_tactic_expr) abstract_argument_type
+
+type declaration_hook = Decl_kinds.strength -> global_reference -> unit
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 321a7b2ec6..c140aec930 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -68,15 +68,15 @@ let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
 let pf_interp_constr gls c =
   let evc = project gls in 
-  Astterm.interp_constr evc (pf_env gls) c
+  Constrintern.interp_constr evc (pf_env gls) c
 
 let pf_interp_openconstr gls c =
   let evc = project gls in 
-  Astterm.interp_openconstr evc (pf_env gls) c
+  Constrintern.interp_openconstr evc (pf_env gls) c
 
 let pf_interp_type gls c =
   let evc = project gls in 
-  Astterm.interp_type evc (pf_env gls) c
+  Constrintern.interp_type evc (pf_env gls) c
 
 let pf_global gls id = Declare.construct_reference (Some (pf_hyps gls)) id
 
@@ -215,223 +215,6 @@ let rename_bound_var_goal gls =
   let ids = ids_of_named_context sign in
   convert_concl (rename_bound_var (Global.env()) ids cl) 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. 
-   They transform the Coqast.t arguments of the tactic into 
-   constr arguments *)
-
-type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic)
-
-(********************************************************)
-(* Functions for hiding the implementation of a tactic. *)
-(********************************************************)
-
-(* hide_tactic s tac pr registers a tactic s under the name s *)
-
-let hide_tactic  s tac  =
-  add_tactic s tac;
-  (fun args -> vernac_tactic(s,args))
-
-(* overwriting_register_tactic s tac pr registers a tactic s under the
-   name s even if a tactic of the same name is already registered *)
-
-let overwrite_hidden_tactic s tac  =
-  overwriting_add_tactic s tac;
-  (fun args -> vernac_tactic(s,args))
-
-let tactic_com = 
-  fun tac t x -> tac (pf_interp_constr x t) x
-
-let tactic_opencom = 
-  fun tac t x -> tac (pf_interp_openconstr x t) x
-      
-let tactic_com_sort = 
-  fun tac t x -> tac (pf_interp_type x t) x
-      
-let tactic_com_list =    
-  fun tac tl x -> 
-    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 
-    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) 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, 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 = 
-  add_tactic s (function [] -> tac | _ -> assert false);
-  vernac_tactic(s,[])
-
-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 CONSTR"
-  in 
-  add_tactic s tacfun;
-  (fun c -> vernac_tactic(s,[Constr c]),
-   (* 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)*)
-    | _ -> 
-	anomaly 
-	  "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 _ -> 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 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 CONSTR"
-  in 
-  add_tactic s tacfun;
-  (fun c  -> vernac_tactic(s,[(OpenConstr c)]))
-
-let hide_numarg_tactic s tac =
-  let tacfun = (function [Integer n] -> tac n | _ -> assert false) in 
-  add_tactic s tacfun;
-  fun n -> vernac_tactic(s,[Integer n])
-
-let hide_ident_tactic s tac =
-  let tacfun = (function [Identifier id] -> tac id | _ -> assert false) in
-  add_tactic s tacfun;
-  fun id -> vernac_tactic(s,[Identifier id])
-      
-let hide_string_tactic s tac =
-  let tacfun = (function [Quoted_string str] -> tac str | _ -> assert false) in
-  add_tactic s tacfun;
-  fun str -> vernac_tactic(s,[Quoted_string str])
-
-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 -> 
-      	tactic_com_list tac 
-          (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 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*)
-    | [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)*)
-    | [Constr c; Cbindings al]  -> tac (c,al)
-    | _ -> 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)*)
-    | []                                ->  [] 
-    | _ -> anomaly "hide_cbindll_tactic : not the expected form" 
-  in  
-  let rec getconstrbinds = function
-    | ((Constr c)::(Cbindings al)::l) -> (c,al)::(getconstrbinds l)
-    | []                              ->  [] 
-    | _ -> anomaly "hide_cbindll_tactic : not the expected form" 
-  in  
-  let rec putconstrbinds = function 
-    | (c,binds)::l -> (Constr c)::(Cbindings binds)::(putconstrbinds l)
-    |  []          -> [] 
-  in
-  let tacfun = function 
-(*    | ((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 CONSTR"
-  in 
-  add_tactic s tacfun;
-  fun l -> vernac_tactic(s,putconstrbinds l)
-*)
-
 (* Pretty-printers *)
 
 open Pp
@@ -442,7 +225,7 @@ open Rawterm
 let pr_com sigma goal com =
   prterm (rename_bound_var (Global.env())
             (ids_of_named_context goal.evar_hyps) 
-            (Astterm.interp_constr sigma (Evarutil.evar_env goal) com))
+            (Constrintern.interp_constr sigma (Evarutil.evar_env goal) com))
 
 let pr_one_binding sigma goal = function
   | (NamedHyp id,com) -> pr_id id ++ str ":=" ++ pr_com sigma goal com
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 49a2db4197..ec849662f6 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -54,8 +54,8 @@ val pf_check_type         : goal sigma -> constr -> types -> unit
 val pf_execute            : goal sigma -> constr -> unsafe_judgment
 val hnf_type_of           : goal sigma -> constr -> types
 
-val pf_interp_constr      : goal sigma -> Coqast.t -> constr
-val pf_interp_type        : goal sigma -> Coqast.t -> types
+val pf_interp_constr      : goal sigma -> Topconstr.constr_expr -> constr
+val pf_interp_type        : goal sigma -> Topconstr.constr_expr -> types
 
 val pf_get_hyp            : goal sigma -> identifier -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> identifier -> types
@@ -77,7 +77,7 @@ val pf_nf_betaiota             : goal sigma -> constr -> constr
 val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
 val pf_reduce_to_atomic_ind     : goal sigma -> types -> inductive * types
 val pf_compute                 : goal sigma -> constr -> constr
-val pf_unfoldn    : (int list * Closure.evaluable_global_reference) list
+val pf_unfoldn    : (int list * evaluable_global_reference) list
         -> goal sigma -> constr -> constr
 
 val pf_const_value : goal sigma -> constant -> constr
@@ -154,39 +154,12 @@ val tactic_list_tactic : tactic_list -> tactic
 val tclFIRSTLIST       : tactic_list list -> tactic_list
 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. *)
-
-type ('a,'b) parse_combinator = ('a -> tactic) -> ('b -> tactic)
-
-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 :
-  (constr substitution, Coqast.t substitution) parse_combinator
-
-val tactic_com_bind_list : 
-  (constr   * constr substitution,
-   Coqast.t * Coqast.t substitution) parse_combinator
-
-val tactic_com_bind_list_list :  
-  ((constr   * constr substitution) list, 
-   (Coqast.t * Coqast.t substitution) list) parse_combinator
-
 (*s Pretty-printing functions. *)
 
 (*i*)
 open Pp
 (*i*)
 
-val pr_com    : evar_map -> goal -> Coqast.t -> std_ppcmds
+val pr_com    : evar_map -> goal -> Topconstr.constr_expr -> std_ppcmds
 val pr_gls    : goal sigma -> std_ppcmds
 val pr_glls   : goal list sigma -> std_ppcmds