Achèvement suppression traducteur dans contrib/interface

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

15 files changed, 49 insertions, 545 deletions

diff --git a/Makefile b/Makefile
index 09265105c4..4678b56476 100644
--- a/Makefile
+++ b/Makefile
@@ -37,7 +37,7 @@ NOARG:
 	@echo "For make to be verbose, add VERBOSE=1"
 
 # build and install the three subsystems: coq, coqide, pcoq
-world: coq coqide # pcoq
+world: coq coqide pcoq
 
 install: install-coq install-coqide install-pcoq
 #install-manpages: install-coq-manpages install-pcoq-manpages
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 8078831152..78716435c1 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -1,13 +1,11 @@
 (* Une tactique qui tente de démontrer toute seule le but courant,
    interruptible par pcoq (si dans le fichier C:\WINDOWS\free il y a un A)
 *)
-open Ctast;;
 open Termops;;
 open Nameops;;
 open Auto;;
 open Clenv;;
 open Command;;
-open Ctast;;
 open Declarations;;
 open Declare;;
 open Eauto;;
@@ -597,7 +595,7 @@ let blast_tac display_function = function
 
 let blast_tac_txt = 
   blast_tac
-    (function x -> msgnl(Pptactic.pr_glob_tactic (Tacinterp.glob_tactic x)));;
+    (function x -> msgnl(Pptacticnew.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));;
 
 (* Obsolète ?
 overwriting_add_tactic "Blast1" blast_tac_txt;;
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index e2edbd8ba7..80dc1a40fd 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -4,7 +4,6 @@
 open Names;;
 open Nameops;;
 open Util;;
-open Ast;;
 open Term;;
 open Pp;;
 open Libnames;;
@@ -13,7 +12,6 @@ open Library;;
 open Vernacinterp;;
 open Evd;;
 open Proof_trees;;
-open Termast;;
 open Tacmach;;
 open Pfedit;;
 open Proof_type;;
@@ -28,7 +26,6 @@ open Vernacinterp;;
 open Vernac;;
 open Command;;
 open Protectedtoplevel;;
-open Coqast;;
 open Line_oriented_parser;;
 open Xlate;;
 open Vtp;;
@@ -283,15 +280,12 @@ let print_check judg =
  let value_ct_ast = 
      (try translate_constr false (Global.env()) value 
       with UserError(f,str) ->
-           raise(UserError(f,
-			   Ast.print_ast 
-				(ast_of_constr true (Global.env()) value) ++
+           raise(UserError(f,Printer.prterm value ++
 			      fnl () ++ str ))) in
  let type_ct_ast =
      (try translate_constr false (Global.env()) typ
       with UserError(f,str) ->
-           raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env())
-					       value) ++ fnl() ++ str))) in
+           raise(UserError(f, Printer.prterm value ++ fnl() ++ str))) in
  ((ctf_SearchResults !global_request_id),
  (Some  (P_pl
   (CT_premises_list
@@ -315,18 +309,6 @@ and ntyp = nf_betaiota typ in
 
 
 
-(* The following function is copied from globpr in env/printer.ml *)
-let globcv x =
-    match x with
-      | Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
-	    convert_qualid
-	      (Nametab.shortest_qualid_of_global Idset.empty (IndRef(sp,tyi)))
-      | Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
-	  convert_qualid
-            (Nametab.shortest_qualid_of_global Idset.empty
-	       (ConstructRef ((sp, tyi), i)))
-  | _ -> failwith "globcv : unexpected value";;
-
 let pbp_tac_pcoq =
     pbp_tac (function (x:raw_tactic_expr) -> 
       output_results
@@ -364,7 +346,7 @@ let debug_tac2_pcoq tac =
 	  (errorlabstrm "DEBUG TACTIC"
 	     (str "no error here " ++ fnl () ++ Printer.pr_goal (sig_it g) ++
 	      fnl () ++ str "the tactic is" ++ fnl () ++
-	      Pptactic.pr_glob_tactic tac);
+	      Pptacticnew.pr_glob_tactic (Global.env()) tac);
 	   result)
 	with
 	  e ->
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
deleted file mode 100644
index 67279bb828..0000000000
--- a/contrib/interface/ctast.ml
+++ /dev/null
@@ -1,76 +0,0 @@
-(* A copy of pre V7 ast *)
-
-open Names
-open Libnames
-
-type loc = Util.loc
-
-type t =
-  | Node of loc * string * t list
-  | Nvar of loc * string
-  | Slam of loc * string option * t
-  | Num of loc * int
-  | Id of loc * string
-  | Str of loc * string
-  | Path of loc * string list
-  | Dynamic of loc * Dyn.t
-
-let section_path sl =
-  match List.rev sl with
-    | s::pa ->
-	Libnames.encode_kn
-	  (make_dirpath (List.map id_of_string pa))
-	  (id_of_string s)
-    | [] -> invalid_arg "section_path"
-
-let is_meta s = String.length s > 0 && s.[0] == '$'
-
-let purge_str s =
-  if String.length s == 0 || s.[0] <> '$' then s
-  else String.sub s 1 (String.length s - 1)
-
-let rec ct_to_ast = function
-  | Node (loc,a,b) -> Coqast.Node (loc,a,List.map ct_to_ast b)
-  | Nvar (loc,a) ->
-      if is_meta a then Coqast.Nmeta (loc,purge_str a)
-      else Coqast.Nvar (loc,id_of_string a)
-  | Slam (loc,Some a,b) ->
-      if is_meta a then Coqast.Smetalam (loc,purge_str a,ct_to_ast b)
-      else Coqast.Slam (loc,Some (id_of_string a),ct_to_ast b)
-  | Slam (loc,None,b) -> Coqast.Slam (loc,None,ct_to_ast b)
-  | Num (loc,a) -> Coqast.Num (loc,a)
-  | Id (loc,a) -> Coqast.Id (loc,a)
-  | Str (loc,a) -> Coqast.Str (loc,a)
-  | Path (loc,sl) -> Coqast.Path (loc,section_path sl)
-  | Dynamic (loc,a) -> Coqast.Dynamic (loc,a)
-
-let rec ast_to_ct = function x -> failwith "ast_to_ct: not TODO?"
-(*
-  | Coqast.Node (loc,a,b) -> Node (loc,a,List.map ast_to_ct b)
-  | Coqast.Nvar (loc,a) -> Nvar (loc,string_of_id a)
-  | Coqast.Nmeta (loc,a) -> Nvar (loc,"$"^a)
-  | Coqast.Slam (loc,Some a,b) ->
-   Slam (loc,Some (string_of_id a),ast_to_ct b)
-  | Coqast.Slam (loc,None,b) -> Slam (loc,None,ast_to_ct b)
-  | Coqast.Smetalam (loc,a,b) -> Slam (loc,Some ("$"^a),ast_to_ct b)
-  | Coqast.Num (loc,a) -> Num (loc,a)
-  | Coqast.Id (loc,a) -> Id (loc,a)
-  | Coqast.Str (loc,a) -> Str (loc,a)
-  | Coqast.Path (loc,a) ->
-    let (sl,bn) = Libnames.decode_kn a in
-    Path(loc, (List.map string_of_id
-                (List.rev (repr_dirpath sl))) @ [string_of_id bn])
-  | Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
-*)
-
-let loc = function
-  | Node (loc,_,_) -> loc
-  | Nvar (loc,_) -> loc
-  | Slam (loc,_,_) -> loc
-  | Num (loc,_) -> loc
-  | Id (loc,_) -> loc
-  | Str (loc,_) -> loc
-  | Path (loc,_) -> loc
-  | Dynamic (loc,_) -> loc
-
-let str s = Str(Util.dummy_loc,s)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index ec98929604..578abc4907 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -251,7 +251,7 @@ let rec sort_list = function
 let mk_dad_meta n = CPatVar (zz,(true,Nameops.make_ident "DAD" (Some n)));;
 let mk_rewrite lr ast =
   let b = in_gen rawwit_bool lr in
-  let cb = in_gen rawwit_constr_with_bindings ((*Ctast.ct_to_ast*) ast,NoBindings) in
+  let cb = in_gen rawwit_constr_with_bindings (ast,NoBindings) in
   TacExtend (zz,"Rewrite",[b;cb])
 
 open Vernacexpr
diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4
index b02b06e866..a7ea5ea624 100644
--- a/contrib/interface/debug_tac.ml4
+++ b/contrib/interface/debug_tac.ml4
@@ -1,7 +1,5 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-open Ast;;
-open Coqast;;
 open Tacmach;;
 open Tacticals;;
 open Proof_trees;;
@@ -12,6 +10,8 @@ open Proof_type;;
 open Tacexpr;;
 open Genarg;;
 
+let pr_glob_tactic = Pptacticnew.pr_glob_tactic (Global.env())
+
 (* Compacting and uncompacting proof commands *)
 
 type report_tree =
@@ -72,11 +72,6 @@ let check_subgoals_count2
 	 Recursive_fail (List.hd !new_report_holder)));
     result;;
 
-(*
-let traceable = function
-    Node(_, "TACTICLIST", a::b::tl) -> true
-  | _ -> false;;
-*)
 let traceable = function
   | TacThen _ | TacThens _ -> true
   | _ -> false;;
@@ -116,25 +111,6 @@ let count_subgoals2
     result;;
 
 let rec local_interp : glob_tactic_expr -> report_holder -> tactic = function
-(*
-    Node(_, "TACTICLIST", [a;Node(_, "TACLIST", l)]) ->
-      (fun report_holder -> checked_thens report_holder a l)
-  | Node(_, "TACTICLIST", a::((Node(_, "TACLIST", l))as b)::c::tl) ->
-      local_interp(ope ("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
-  | Node(_, "TACTICLIST", [a;b]) ->
-      (fun report_holder -> checked_then report_holder a b)
-  | Node(_, "TACTICLIST", a::b::c::tl) ->
-	local_interp(ope ("TACTICLIST", (ope("TACTICLIST", [a;b]))::c::tl))
-  | ast ->
-      (fun report_holder g ->
-	try
-	  let (gls, _) as result = Tacinterp.interp ast g in
-	  report_holder := (Report_node(true, List.length (sig_it gls), []))
-			    ::!report_holder;
-	  result
-	with e -> (report_holder := (Failed 1)::!report_holder;
-		   tclIDTAC g))
-*)
     TacThens (a,l) ->
       (fun report_holder -> checked_thens report_holder a l)
   | TacThen (a,b) ->
@@ -288,71 +264,11 @@ let mkOnThen t1 t2 selected_indices =
 
 (* Analyzing error reports *)
 
-(*
-let rec select_success n = function
-    [] -> []
-  | Report_node(true,_,_)::tl -> (Num((0,0),n))::select_success (n+1) tl
-  | _::tl -> select_success (n+1) tl;;
-*)
 let rec select_success n = function
     [] -> []
   | Report_node(true,_,_)::tl -> n::select_success (n+1) tl
   | _::tl -> select_success (n+1) tl;;
 
-(*
-let rec expand_tactic = function
-    Node(loc1, "TACTICLIST", [a;Node(loc2,"TACLIST", l)]) ->
-      Node(loc1, "TACTICLIST",
-	   [expand_tactic a;
-	     Node(loc2, "TACLIST", List.map expand_tactic l)])
-  | Node(loc1, "TACTICLIST", a::((Node(loc2, "TACLIST", l))as b)::c::tl) ->
-      expand_tactic (Node(loc1, "TACTICLIST",
-			  (Node(loc1, "TACTICLIST", [a;b]))::c::tl))
-  | Node(loc1, "TACTICLIST", [a;b]) ->
-      Node(loc1, "TACTICLIST",[expand_tactic a;expand_tactic b])
-  | Node(loc1, "TACTICLIST", a::b::c::tl) ->
-      expand_tactic (Node(loc1, "TACTICLIST",
-			  (Node(loc1, "TACTICLIST", [a;b]))::c::tl))
-  | any -> any;;
-*)
-(* Useless: already in binary form...
-let rec expand_tactic = function
-    TacThens (a,l) -> TacThens (expand_tactic a, List.map expand_tactic l)
-  | TacThen (a,b) -> TacThen (expand_tactic a, expand_tactic b)
-  | any -> any;;
-*)
-
-(*
-let rec reconstruct_success_tac ast = 
-  match ast with
-    Node(_, "TACTICLIST", [a;Node(_,"TACLIST",l)]) ->
-      (function 
-	  Report_node(true, n, l) -> ast
-      	| Report_node(false, n, rl) ->
-	    ope("TACTICLIST",[a;ope("TACLIST", 
-				    List.map2 reconstruct_success_tac l rl)])
-      	| Failed n -> ope("Idtac",[])
-      	| Tree_fail r -> reconstruct_success_tac a r
-      	| Mismatch (n,p) -> a)
-  | Node(_, "TACTICLIST", [a;b]) ->
-      (function
-	  Report_node(true, n, l) -> ast
-	| Report_node(false, n, rl) ->
-	    let selected_indices = select_success 1 rl in
-	    ope("OnThen", a::b::selected_indices)
-	| Failed n -> ope("Idtac",[])
-	| Tree_fail r -> reconstruct_success_tac a r
-	| _ -> error "this error case should not happen in a THEN tactic")
-  | _ -> 
-      (function
-	  Report_node(true, n, l) -> ast
-	| Failed n -> ope("Idtac",[])
-	| _ ->
-	    errorlabstrm
-	      "this error case should not happen on an unknown tactic"
-              (str "error in reconstruction with " ++ fnl () ++
-	       (gentacpr ast)));;
-*)
 let rec reconstruct_success_tac (tac:glob_tactic_expr) =
   match tac with
     TacThens (a,l) ->
@@ -396,21 +312,6 @@ let rec path_to_first_error = function
     p::(path_to_first_error t)
 | _ -> [];;
 
-(*
-let rec flatten_then_list tail = function
-  | Node(_, "TACTICLIST", [a;b]) ->
-      flatten_then_list ((flatten_then b)::tail) a
-  | ast -> ast::tail
-and flatten_then = function
-    Node(_, "TACTICLIST", [a;b]) ->
-      ope("TACTICLIST", flatten_then_list [flatten_then b] a)
-  | Node(_, "TACLIST", l) ->
-      ope("TACLIST", List.map flatten_then l)
-  | Node(_, "OnThen", t1::t2::l) ->
-      ope("OnThen", (flatten_then t1)::(flatten_then t2)::l)
-  | ast -> ast;;
-*)
-
 let debug_tac = function
     [(Tacexp ast)] ->
       (fun g -> 
@@ -435,26 +336,8 @@ let debug_tac = function
 add_tactic "DebugTac" debug_tac;;
 *)
 
-(*
-hide_tactic "OnThen" on_then;;
-*)
 Refiner.add_tactic "OnThen" on_then;;
 
-(*
-let rec clean_path p ast l = 
-  match ast, l with
-    Node(_, "TACTICLIST", ([_;_] as tacs)), fst::tl ->
-       fst::(clean_path 0 (List.nth tacs (fst - 1)) tl)
-  | Node(_, "TACTICLIST", tacs), 2::tl ->
-     let rank = (List.length tacs) - p in
-     rank::(clean_path 0 (List.nth tacs (rank - 1)) tl)
-  | Node(_, "TACTICLIST", tacs), 1::tl ->
-      clean_path (p+1) ast tl
-  | Node(_, "TACLIST", tacs), fst::tl ->
-      fst::(clean_path 0 (List.nth tacs (fst - 1)) tl)
-  | _, [] -> []
-  | _, _ -> failwith "this case should not happen in clean_path";;
-*)
 let rec clean_path tac l = 
   match tac, l with
   | TacThen (a,b), fst::tl ->
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 0add95076a..97f2602d8b 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -2,9 +2,6 @@ open Sign;;
 open Classops;;
 open Names;;
 open Nameops
-open Coqast;;
-open Ast;;
-open Termast;;
 open Term;;
 open Impargs;;
 open Reduction;;
@@ -90,13 +87,6 @@ let implicit_args_to_ast_list sp mipv =
 	  [] -> []
 	| _ -> [VernacComments (List.rev implicit_args_descriptions)];;
 	      
-let convert_qualid qid =
-  let d, id = Libnames.repr_qualid qid in
-    match repr_dirpath d with
-	[] -> nvar id
-      | d -> ope("QUALID", List.fold_left (fun l s -> (nvar s)::l)
-		   [nvar id] d);;
-
 (* This function converts constructors for an inductive definition to a
    Coqast.t.  It is obtained directly from print_constructors in pretty.ml *)
 
@@ -142,16 +132,6 @@ let implicits_to_ast_list implicits =
     | None -> []
     | Some s -> [VernacComments [CommentString s]];;
 
-(*
-let make_variable_ast name typ implicits =
-   (ope("VARIABLE",
-    [string "VARIABLE";
-     ope("BINDERLIST",
-         [ope("BINDER",
-            [(constr_to_ast (body_of_type typ));
-             nvar name])])]))::(implicits_to_ast_list implicits)
-    ;;
-*)
 let make_variable_ast name typ implicits =
   (VernacAssumption
     ((Local,Definitional),
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index 0eca0a1e77..b8c2d7dc71 100644
--- a/contrib/interface/name_to_ast.mli
+++ b/contrib/interface/name_to_ast.mli
@@ -1,2 +1 @@
 val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;;
-val convert_qualid : Libnames.qualid -> Coqast.t;;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 7728cf48ab..1e1d7cb4e1 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -48,52 +48,6 @@ let ctf_FileErrorMessage reqid pps =
   int reqid ++ fnl () ++ pps ++ fnl () ++ str "E-n-d---M-e-s-s-a-g-e" ++
   fnl ();;
 
-(*
-(*In the code for CoqV6.2, the require_module call is encapsulated in
-  a function "without_mes_ambig".  Here I have supposed that this
-  function has no effect on parsing *)
-let try_require_module import specif names =
- try Library.require_module 
-   (if specif = "UNSPECIFIED" then None
-    else Some (specif = "SPECIFICATION"))
-   (List.map 
-     (fun name ->
-       (dummy_loc,Libnames.make_short_qualid (Names.id_of_string name)))
-      names)
-   (import = "IMPORT")
- with
-   | e -> msgnl (str "Reinterning of " ++ prlist str names ++ str " failed");;
-*)
-(*
-let try_require_module_from_file import specif name fname =
- try Library.require_module_from_file (if specif = "UNSPECIFIED" then None
-  else Some (specif = "SPECIFICATION")) (Some (Names.id_of_string name)) fname (import = "IMPORT")
- with
- | e -> msgnl (str "Reinterning of " ++ str name ++ str " failed");;
-*)
-(*
-let execute_when_necessary ast =
- (match ast with
-  | Node (_, "GRAMMAR", ((Nvar (_, s)) :: ((Node (_, "ASTLIST", al)) :: []))) ->
-   Metasyntax.add_grammar_obj s (List.map Ctast.ct_to_ast al)
-(* Obsolete
-  | Node (_, "TOKEN", ((Str (_, s)) :: [])) -> Metasyntax.add_token_obj s
-*)
-  | Node (_, "Require",
-            ((Str (_, import)) ::
-              ((Str (_, specif)) :: l))) ->
-   let mnames = List.map (function
-     | (Nvar (_, m)) -> m
-     | _ -> error "parse_string_action : bad require expression") l in
-   try_require_module import specif mnames
-  | Node (_, "RequireFrom",
-            ((Str (_, import)) ::
-              ((Str (_, specif)) ::
-                ((Nvar (_, mname)) :: ((Str (_, file_name)) :: []))))) ->
-   try_require_module_from_file import specif mname file_name
-  | _ -> ()); ast;;
-*)
-
 let execute_when_necessary v =
  (match v with
   | VernacOpenCloseScope sc -> Vernacentries.interp v
@@ -201,12 +155,6 @@ let parse_command_list reqid stream string_list =
                 discard_to_dot stream;
                 msgnl (str "debug" ++ fnl () ++ int this_pos ++ fnl () ++
 		       int (Stream.count stream));
-(*
-                Some( Node(l, "PARSING_ERROR",
-                        List.map Ctast.str
-                        (get_substring_list string_list this_pos
-                            (Stream.count stream))))
-*)
 		ParseError ("PARSING_ERROR",
                   get_substring_list string_list this_pos
 		    (Stream.count stream))
@@ -215,12 +163,6 @@ let parse_command_list reqid stream string_list =
         | e-> 
           begin
             discard_to_dot stream;
-(*
-            Some(Node((0,0), "PARSING_ERROR2",
-                   List.map Ctast.str
-		   (get_substring_list string_list this_pos
-                     (Stream.count stream))))
-*)
 	    ParseError ("PARSING_ERROR2",
 	      get_substring_list string_list this_pos (Stream.count stream))
           end in
@@ -229,13 +171,6 @@ let parse_command_list reqid stream string_list =
         let ast0 = (execute_when_necessary ast) in
           (try xlate_vernac ast
 	  with e ->
-(*
-	    xlate_vernac 
-              (Node((0,0), "PARSING_ERROR2",
-               List.map Ctast.str
-		 (get_substring_list string_list this_pos
-		    (Stream.count stream)))))::parse_whole_stream()
-*)
 	    make_parse_error_item "PARSING_ERROR2" 
 		     (get_substring_list string_list this_pos
 		       (Stream.count stream)))::parse_whole_stream()
@@ -455,7 +390,6 @@ Libobject.relax true;
 	   coqdir [ "contrib"; "interface"; "vernacrc"] in
    try
      (Gramext.warning_verbose := false;
-      Esyntax.warning_verbose := false;
       coqparser_loop (open_in vernacrc))
    with
      | End_of_file -> ()
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 1c89156b55..3ada7cb6db 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -11,7 +11,6 @@ open Term
 open Termops
 open Util
 open Proof_type
-open Coqast
 open Pfedit
 open Translate
 open Term
@@ -163,26 +162,6 @@ let rule_is_complex r =
    |_ -> false
 ;;
 
-let ast_of_constr = Termast.ast_of_constr true (Global.env()) ;;
-
-(*
-let rule_to_ntactic r =
-   let rast =
-     (match r with
-       Tactic (s,l) ->
-	 Ast.ope (s,(List.map ast_of_cvt_arg l))
-     | Prim (Refine h) ->
-	 Ast.ope ("Exact",
-		  [Node ((0,0), "COMMAND", [ast_of_constr h])])
-     | _ -> Ast.ope ("Intros",[])) in
-   if rule_is_complex r
-   then (match rast with
-           Node(_,_,[Node(_,_,[Node(_,_,x)])]) ->x
-          | _ -> assert false)
-
-   else [rast ]
-;;
-*)
 let rule_to_ntactic r =
    let rt =
      (match r with
@@ -197,14 +176,6 @@ let rule_to_ntactic r =
    else rt
 ;;
 
-(*
-let term_of_command x =
-  match x with
-    Node(_,_,y::_) -> y
-  | _ -> x
-;;
-*)
-
 (* Attribue les preuves de la liste l aux sous-buts non-prouvés de nt  *)
 
 
@@ -418,13 +389,6 @@ let enumerate f ln =
 
 let constr_of_ast = Constrintern.interp_constr Evd.empty (Global.env());;
 
-(*
-let sp_tac tac =
-   try spt (constr_of_ast (term_of_command tac))
-   with _ -> (* let Node(_,t,_) = tac in *)
-             spe (* sps ("error in sp_tac " ^ t) *)
-;;
-*)
 let sp_tac tac = failwith "TODO"
 
 let soit_A_une_proposition nh ln t=  match !natural_language with
@@ -964,16 +928,6 @@ let  natural_lhyp lh hi =
     Analyse des tactiques.
 *)
 
-(*
-let name_tactic tac =
-      match tac with
-        (Node(_,"Interp",
-		(Node(_,_,
-		      (Node(_,t,_))::_))::_))::_  -> t
-       |(Node(_,t,_))::_ -> t
-       | _ -> assert false
-;;
-*)
 let name_tactic = function
   | TacIntroPattern _ -> "Intro"
   | TacAssumption -> "Assumption"
@@ -992,51 +946,8 @@ let arg1_tactic tac =
 ;;
 *)
 
-let arg1_tactic tac = failwith "TODO"
-
-let arg2_tactic tac =
-   match tac with
-     (Node(_,"Interp",
-		(Node(_,_,
-		      (Node(_,_,_::x::_))::_))::_))::_ -> x
-    | (Node(_,_,_::x::_))::_ -> x
-    | _ -> assert false
-;;
-
-(*
-type nat_tactic =
-    Split of (Coqast.t list)
-  | Generalize of (Coqast.t list)
-  | Reduce of string*(Coqast.t list)
-  | Other of string*(Coqast.t list)
-;;
-
-let analyse_tac tac =
-  match tac with
-    [Node (_, "Split", [Node (_, "BINDINGS", [])])]
-      -> Split []
-  | [Node (_, "Split",[Node(_, "BINDINGS",[Node(_, "BINDING",
-	[Node (_, "COMMAND", x)])])])] 
-     -> Split x
-  | [Node (_, "Generalize", [Node (_, "COMMAND", x)])] 
-     ->Generalize x
-  | [Node (_, "Reduce", [Node (_, "REDEXP", [Node (_, mode, _)]);
-             Node (_, "CLAUSE", lhyp)])] 
-     -> Reduce(mode,lhyp)
-  | [Node (_, x,la)] -> Other (x,la)
-  | _ -> assert false
-;;
-*)
-      
-
-
+let arg1_tactic tac = failwith "TODO";;
 
-
-let id_of_command x =
-  match x with
-      Node(_,_,Node(_,_,y::_)::_) ->  y
-     |_ -> assert false
-;;
 type type_info_subgoals =
     {ihsg: type_info_subgoals_hyp;
      isgintro : string}
@@ -1286,7 +1197,7 @@ let rec natural_ntree ig ntree =
 	  | TacAssumption -> natural_trivial ig lh g gs ltree
 	  | TacClear _ -> natural_clear ig lh g gs ltree
 (* Besoin de l'argument de la tactique *)
-	  | TacSimpleInduction (NamedHyp id,_) -> 
+	  | TacSimpleInduction (NamedHyp id) -> 
               natural_induction ig lh g gs ge id ltree false
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
diff --git a/contrib/interface/showproof.mli b/contrib/interface/showproof.mli
index ee2694585f..9b6787b7c7 100755
--- a/contrib/interface/showproof.mli
+++ b/contrib/interface/showproof.mli
@@ -4,9 +4,7 @@ open Names
 open Term
 open Util
 open Proof_type
-open Coqast
 open Pfedit
-open Translate
 open Term
 open Reduction
 open Clenv
diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml
index ee901c5e7c..f6ab47376b 100644
--- a/contrib/interface/showproof_ct.ml
+++ b/contrib/interface/showproof_ct.ml
@@ -3,7 +3,6 @@
    Vers Ctcoq
 *)
 
-open Esyntax
 open Metasyntax
 open Printer
 open Pp
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index e63baecfb5..6e4782be09 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -1,13 +1,11 @@
 open Names;;
 open Sign;;
 open Util;;
-open Ast;;
 open Term;;
 open Pp;;
 open Libobject;;
 open Library;;
 open Vernacinterp;;
-open Termast;;
 open Tacmach;;
 open Pfedit;;
 open Parsing;;
@@ -15,97 +13,11 @@ open Evd;;
 open Evarutil;;
 
 open Xlate;;
-open Ctast;;
 open Vtp;;
 open Ascent;;
 open Environ;;
 open Proof_type;;
 
-(* dead code: let rel_reference gt k oper = 
- if is_existential_oper oper then ope("XTRA", [str "ISEVAR"])
- else begin
-  let id = id_of_global oper in
-  let oper', _ = global_operator (Nametab.sp_of_id k id) id in
-  if oper = oper' then nvar (string_of_id id)
-  else failwith "xlate"
-end;;
-*)
-
-(* dead code: 
-let relativize relfun =
- let rec relrec =
-  function
-     | Nvar (_, id) -> nvar id
-     | Slam (l, na, ast) -> Slam (l, na, relrec ast)
-     | Node (loc, nna, l) as ast -> begin
-       try relfun ast
-       with
-       | Failure _ -> Node (loc, nna, List.map relrec l)
-     end
-     | a -> a in
- relrec;;
-*)
-
-(* dead code:
-let dbize_sp =
- function
-    | Path (loc, sl, s) -> begin
-      try section_path sl s
-      with
-      | Invalid_argument _ | Failure _ ->
-      anomaly_loc
-       (loc, "Translate.dbize_sp (taken from Astterm)",
-       [< str "malformed section-path" >])
-    end
-    | ast ->
-     anomaly_loc
-      (Ast.loc ast, "Translate.dbize_sp (taken from Astterm)",
-      [< str "not a section-path" >]);;
-*)
-
-(* dead code:
-let relativize_cci gt = relativize (function
-    | Node (_, "CONST", (p :: _)) as gt ->
-     rel_reference gt CCI (Const (dbize_sp p))
-    | Node (_, "MUTIND", (p :: ((Num (_, tyi)) :: _))) as gt ->
-     rel_reference gt CCI (MutInd (dbize_sp p, tyi))
-    | Node (_, "MUTCONSTRUCT", (p :: ((Num (_, tyi)) :: ((Num (_, i)) :: _)))) as gt ->
-     rel_reference gt CCI (MutConstruct (
-      (dbize_sp p, tyi), i))
-    | _ -> failwith "caught") gt;;
-*)
-
-let coercion_description_holder = ref (function _ -> None : t -> int option);;
-
-let coercion_description t = !coercion_description_holder t;;
-
-let set_coercion_description f =
- coercion_description_holder:=f; ();;
-
-let rec nth_tl l n = if n = 0 then l
- else (match l with
- | a :: b -> nth_tl b (n - 1)
- | [] -> failwith "list too short for nth_tl");;
-
-let rec discard_coercions =
- function
-    | Slam (l, na, ast) -> Slam (l, na, discard_coercions ast)
-    | Node (l, ("APPLIST" as nna), (f :: args as all_sons)) ->
-     (match coercion_description f with
-     | Some n ->
-      let new_args =
-       try nth_tl args n
-       with
-       | Failure "list too short for nth_tl" -> [] in
-      (match new_args with
-       | a :: (b :: c) -> Node (l, nna, List.map discard_coercions new_args)
-       | a :: [] -> discard_coercions a
-       | [] -> Node (l, nna, List.map discard_coercions all_sons))
-     | None -> Node (l, nna, List.map discard_coercions all_sons))
-    | Node (l, nna, all_sons) ->
-     Node (l, nna, List.map discard_coercions all_sons)
-    | it -> it;;
-
 (*translates a formula into a centaur-tree --> FORMULA *)
 let translate_constr at_top env c =
   xlate_formula (Constrextern.extern_constr at_top env c);;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b4e106a4d8..1439d4cd12 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -369,14 +369,11 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CApp(_, (_,f), l) -> 
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
    | CCases (_, _, [], _) -> assert false
-   | CCases (_, (Some _, _), _, _) -> xlate_error "NOT parsed: Cases with Some"
-   | CCases (_,(None, ret_type), tm::tml, eqns)->
+   | CCases (_, ret_type, tm::tml, eqns)->
        CT_cases(CT_matched_formula_ne_list(xlate_matched_formula tm,
 					   List.map xlate_matched_formula tml),
 		xlate_formula_opt ret_type,
                 CT_eqn_list (List.map (fun x -> translate_one_equation x) eqns))
-   | COrderedCase (_,Term.IfStyle,po,c,[b1;b2]) -> 
-       xlate_error "No more COrderedCase"
    | CLetTuple (_,a::l, ret_info, c, b) -> 
       CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
 				     List.map xlate_id_opt_aux l),
@@ -389,13 +386,6 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	 (xlate_formula c, xlate_return_info ret_info,
 	  xlate_formula b1, xlate_formula b2)
 
-   | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
-       CT_inductive_let(xlate_formula_opt po,
-	       xlate_id_opt_ne_list l,
-	       xlate_formula c, xlate_formula b) 
-   | COrderedCase (_,c,v,e,l) -> 
-	 CT_elimc(CT_case "Case", xlate_formula_opt v, xlate_formula e,
-		  CT_formula_list(List.map xlate_formula l))
    | CSort(_, s) -> CT_coerce_SORT_TYPE_to_FORMULA(xlate_sort s)
    | CNotation(_, s, l) -> notation_to_formula s (List.map xlate_formula l)
    | CNumeral(_, i) -> 
@@ -426,8 +416,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
      let strip_mutrec (fid, n, bl, arf, ardef) =
         let (struct_arg,bl,arf,ardef) =
          if bl = [] then
-           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
-           let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+           let (bl,arf,ardef) = Ppconstrnew.split_fix (n+1) arf ardef in
            (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
          else (make_fix_struct (n, bl),bl,arf,ardef) in
         let arf = xlate_formula arf in
@@ -478,14 +467,14 @@ let xlate_hyp = function
 
 let xlate_hyp_location =
  function
-  | AI (_,id), nums, (InHypTypeOnly,_) ->
+  | AI (_,id), nums, InHypTypeOnly ->
       CT_intype(xlate_ident id, nums_to_int_list nums)
-  | AI (_,id), nums, (InHypValueOnly,_) ->
+  | AI (_,id), nums, InHypValueOnly ->
       CT_invalue(xlate_ident id, nums_to_int_list nums)
-  | AI (_,id), [], (InHyp,_) ->
+  | AI (_,id), [], InHyp ->
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_coerce_ID_to_UNFOLD (xlate_ident id))
-  | AI (_,id), a::l, (InHyp,_) ->
+  | AI (_,id), a::l, InHyp ->
       CT_coerce_UNFOLD_to_HYP_LOCATION 
 	(CT_unfold_occ (xlate_ident id, 
 			CT_int_ne_list(CT_int a, nums_to_int_list_aux l)))
@@ -914,7 +903,7 @@ and xlate_tac =
      CT_discriminate_eq
          (xlate_quantified_hypothesis_opt
 	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
-    | TacExtend (_,"deq", [idopt]) ->
+    | TacExtend (_,"simplify_eq", [idopt]) ->
 	let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in
 	let idopt2 = match idopt1 with
 	    None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT
@@ -972,46 +961,46 @@ and xlate_tac =
      let c = xlate_formula c and bindl = xlate_bindings bindl in
      if b then CT_rewrite_lr (c, bindl, ctv_ID_OPT_NONE)
      else CT_rewrite_rl (c, bindl, ctv_ID_OPT_NONE)
-    | TacExtend (_,"rewritein", [b; cbindl; id]) ->
+    | TacExtend (_,"rewrite_in", [b; cbindl; id]) ->
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_formula c and bindl = xlate_bindings bindl in
-     let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
+     let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
      if b then CT_rewrite_lr (c, bindl, id)
      else CT_rewrite_rl (c, bindl, id)
-    | TacExtend (_,"conditionalrewrite", [t; b; cbindl]) ->
+    | TacExtend (_,"conditional_rewrite", [t; b; cbindl]) ->
      let t = out_gen rawwit_main_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_formula c and bindl = xlate_bindings bindl in
      if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
      else CT_condrewrite_rl (xlate_tactic t, c, bindl, ctv_ID_OPT_NONE)
-    | TacExtend (_,"conditionalrewrite", [t; b; cbindl; id]) ->
+    | TacExtend (_,"conditional_rewrite", [t; b; cbindl; id]) ->
      let t = out_gen rawwit_main_tactic t in
      let b = out_gen Extraargs.rawwit_orient b in
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_formula c and bindl = xlate_bindings bindl in
-     let id = ctf_ID_OPT_SOME (xlate_ident (out_gen rawwit_ident id)) in
+     let id = ctf_ID_OPT_SOME (xlate_ident (snd (out_gen rawwit_var id))) in
      if b then CT_condrewrite_lr (xlate_tactic t, c, bindl, id)
      else CT_condrewrite_rl (xlate_tactic t, c, bindl, id)
-    | TacExtend (_,"dependentrewrite", [b; c]) ->
+    | TacExtend (_,"dependent_rewrite", [b; c]) ->
       let b = out_gen Extraargs.rawwit_orient b in
       let c = xlate_formula (out_gen rawwit_constr c) in
       (match c with
 	| CT_coerce_ID_to_FORMULA (CT_ident _ as id) -> 
 	    if b then CT_deprewrite_lr id else CT_deprewrite_rl id
 	| _ -> xlate_error "dependent rewrite on term: not supported")
-    | TacExtend (_,"dependentrewrite", [b; c; id]) ->
+    | TacExtend (_,"dependent_rewrite", [b; c; id]) ->
 	xlate_error "dependent rewrite on terms in hypothesis: not supported"
-    | TacExtend (_,"cutrewrite", [b; c]) ->
+    | TacExtend (_,"cut_rewrite", [b; c]) ->
       let b = out_gen Extraargs.rawwit_orient b in
       let c = xlate_formula (out_gen rawwit_constr c) in
       if b then CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
       else CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
-    | TacExtend (_,"cutrewrite", [b; c; id]) ->
+    | TacExtend (_,"cut_rewrite", [b; c; id]) ->
       let b = out_gen Extraargs.rawwit_orient b in
       let c = xlate_formula (out_gen rawwit_constr c) in
-      let id = xlate_ident (out_gen rawwit_ident id) in
+      let id = xlate_ident (snd (out_gen rawwit_var id)) in
       if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
       else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
     | TacExtend(_, "subst", [l]) ->
@@ -1115,7 +1104,7 @@ and xlate_tac =
      CT_elim (xlate_formula c1, xlate_bindings sl, xlate_using u)
     | TacCase (c1,sl) ->
      CT_casetac (xlate_formula c1, xlate_bindings sl)
-    | TacSimpleInduction (h,_) -> CT_induction (xlate_quantified_hypothesis h)
+    | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
     | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
     | TacCut c -> CT_cut (xlate_formula c)
     | TacLApply c -> CT_use (xlate_formula c)
@@ -1153,11 +1142,11 @@ and xlate_tac =
 	CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l))
     | TacDAuto (a, b) ->
 	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
-    | TacNewDestruct(a,b,(c,_)) ->
+    | TacNewDestruct(a,b,c) ->
 	CT_new_destruct
 	  (xlate_int_or_constr a, xlate_using b, 
 	   xlate_intro_patt_opt c)
-    | TacNewInduction(a,b,(c,_)) ->
+    | TacNewInduction(a,b,c) ->
 	CT_new_induction
 	  (xlate_int_or_constr a, xlate_using b,
 	   xlate_intro_patt_opt c)
@@ -1221,8 +1210,11 @@ and coerce_genarg_to_TARG x =
 	CT_coerce_FORMULA_OR_INT_to_TARG
 	  (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
 	     (CT_coerce_ID_to_ID_OR_INT id))
-  | HypArgType ->
-      xlate_error "TODO (similar to IdentArgType)"
+  | VarArgType ->
+      let id = xlate_ident (snd (out_gen rawwit_var x)) in
+	CT_coerce_FORMULA_OR_INT_to_TARG
+	  (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
+	     (CT_coerce_ID_to_ID_OR_INT id))
   | RefArgType ->
       let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
 	CT_coerce_FORMULA_OR_INT_to_TARG
@@ -1315,8 +1307,11 @@ let coerce_genarg_to_VARG x =
       CT_coerce_ID_OPT_OR_ALL_to_VARG
 	      (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
 	        (CT_coerce_ID_to_ID_OPT id))
-  | HypArgType ->
-      xlate_error "TODO (similar to IdentArgType)"
+  | VarArgType ->
+      let id = xlate_ident (snd (out_gen rawwit_var x)) in
+      CT_coerce_ID_OPT_OR_ALL_to_VARG
+	      (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
+	        (CT_coerce_ID_to_ID_OPT id))
   | RefArgType ->
       let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
       CT_coerce_ID_OPT_OR_ALL_to_VARG
@@ -1644,18 +1639,13 @@ let rec xlate_vernac =
 		 CT_add_field(a1, aplus1, amult1, aone1, azero1, aopp1, aeq1,
 			      ainv1, fth1, ainvl1, bind)
 	   |_ -> assert false)
-  | VernacExtend (("HintRewriteV7"|"HintRewriteV8") as key, largs) ->
-      let in_v8 = (key = "HintRewriteV8") in
-      let orient = out_gen Extraargs.rawwit_orient (List.nth largs 0) in
-      let formula_list = out_gen (wit_list1 rawwit_constr) (List.nth largs 1) in
-      let t =
-	if List.length largs = 4 then
-	   out_gen rawwit_main_tactic (List.nth largs (if in_v8 then 2 else 3))
-	 else
-	   TacId "" in
-      let base = 
-	out_gen rawwit_pre_ident
-	  (if in_v8 then last largs else List.nth largs 2) in
+  | VernacExtend ("HintRewrite", o::f::([b]|[_;b] as args)) ->
+      let orient = out_gen Extraargs.rawwit_orient o in
+      let formula_list = out_gen (wit_list1 rawwit_constr) f in
+      let base = out_gen rawwit_pre_ident b in
+      let t = 
+	match args with [t;_] -> out_gen rawwit_main_tactic t | _ -> TacId ""
+      in
       let ct_orient = match orient with
 	| true  -> CT_lr
 	| false -> CT_rl in
@@ -1880,8 +1870,7 @@ let rec xlate_vernac =
       let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
         let (struct_arg,bl,arf,ardef) =
          if bl = [] then
-           let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in
-           let bl = List.map (fun(nal,ty)->LocalRawAssum(nal,ty)) bl in
+           let (bl,arf,ardef) = Ppconstrnew.split_fix (n+1) arf ardef in
            (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef)
          else (make_fix_struct (n, bl),bl,arf,ardef) in
         let arf = xlate_formula arf in
@@ -2033,8 +2022,6 @@ let rec xlate_vernac =
 	(CT_command_list(xlate_vernac a, 
 			 List.map (fun (_, x) -> xlate_vernac x) l))
   | VernacList([]) -> assert false
-  | (VernacV7only _ | VernacV8only _) ->
-      xlate_error "Not treated here"
   | VernacNop -> CT_proof_no_op
   | VernacComments l -> 
       CT_scomments(CT_scomment_content_list (List.map xlate_comment l))
@@ -2125,8 +2112,5 @@ let rec xlate_vernac_list =
    | VernacList (v::l) ->
        CT_command_list
          (xlate_vernac (snd v), List.map (fun (_,x) -> xlate_vernac x) l)
-   | VernacV7only v -> 
-       if !Options.v7 then xlate_vernac_list v
-       else xlate_error "Unknown command"
    | VernacList [] -> xlate_error "xlate_command_list"
    | _ -> xlate_error "Not a list of commands";;
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v
index c919d6d8d5..7d60bbd977 100644
--- a/test-suite/parser/obj_magic.v
+++ b/test-suite/parser/obj_magic.v
@@ -1,5 +1,5 @@
 inversion H.
-ry absurd (exists a : b, c).
+try absurd (exists a : b, c).
 discriminate H.
 simplify_eq H.
 injection H.