Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

21 files changed, 317 insertions, 789 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 61d0d5a3..fb71288a 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -119,11 +119,13 @@ and ct_COMMAND =
   | CT_print_about of ct_ID
   | CT_print_all
   | CT_print_classes
+  | CT_print_ltac of ct_ID
   | CT_print_coercions
   | CT_print_grammar of ct_GRAMMAR
   | CT_print_graph
   | CT_print_hint of ct_ID_OPT
   | CT_print_hintdb of ct_ID_OR_STAR
+  | CT_print_rewrite_hintdb of ct_ID
   | CT_print_id of ct_ID
   | CT_print_implicit of ct_ID
   | CT_print_loadpath
@@ -135,6 +137,7 @@ and ct_COMMAND =
   | CT_print_opaqueid of ct_ID
   | CT_print_path of ct_ID * ct_ID
   | CT_print_proof of ct_ID
+  | CT_print_setoids
   | CT_print_scope of ct_ID
   | CT_print_scopes
   | CT_print_section of ct_ID
@@ -465,8 +468,8 @@ and ct_MODULE_EXPR =
   | CT_module_app of ct_MODULE_EXPR * ct_MODULE_EXPR
 and ct_MODULE_TYPE =
     CT_coerce_ID_to_MODULE_TYPE of ct_ID
-  | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID * ct_FORMULA
-  | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID * ct_ID
+  | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID_LIST * ct_FORMULA
+  | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID_LIST * ct_ID
 and ct_MODULE_TYPE_CHECK =
     CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT
   | CT_only_check of ct_MODULE_TYPE
@@ -530,6 +533,7 @@ and ct_RED_COM =
   | CT_lazy of ct_CONVERSION_FLAG_LIST * ct_CONV_SET
   | CT_pattern of ct_PATTERN_NE_LIST
   | CT_red
+  | CT_cbvvm
   | CT_simpl of ct_PATTERN_OPT
   | CT_unfold of ct_UNFOLD_NE_LIST
 and ct_RETURN_INFO =
@@ -637,6 +641,7 @@ and ct_TACTIC_COM =
   | CT_elim of ct_FORMULA * ct_SPEC_LIST * ct_USING
   | CT_elim_type of ct_FORMULA
   | CT_exact of ct_FORMULA
+  | CT_exact_no_check of ct_FORMULA
   | CT_exists of ct_SPEC_LIST
   | CT_fail of ct_ID_OR_INT * ct_STRING_OPT
   | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list
@@ -665,8 +670,8 @@ and ct_TACTIC_COM =
   | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
   | CT_move_after of ct_ID * ct_ID
-  | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_OPT
-  | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_OPT
+  | CT_new_destruct of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT
+  | CT_new_induction of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT
   | CT_omega
   | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
   | CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list
@@ -679,7 +684,7 @@ and ct_TACTIC_COM =
   | CT_reflexivity
   | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
-  | CT_replace_with of ct_FORMULA * ct_FORMULA
+  | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT
   | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
   | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
   | CT_right of ct_SPEC_LIST
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index d5236a7a..21f977f1 100755..100644
--- 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;;
@@ -38,7 +36,6 @@ open Typing;;
 open Util;;
 open Vernacentries;;
 open Vernacinterp;;
-open Evar_refiner;;
 
 
 let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
@@ -94,7 +91,7 @@ let rec def_const_in_term_rec vl x =
           def_const_in_term_rec vl (mkInd (inductive_of_constructor c))
    | Case(_,x,t,a) 
         -> def_const_in_term_rec vl x
-   | Cast(x,t)-> def_const_in_term_rec vl t
+   | Cast(x,_,t)-> def_const_in_term_rec vl t
    | Const(c)  -> def_const_in_term_rec vl (lookup_constant c vl).const_type
    | _ -> def_const_in_term_rec vl (type_of vl Evd.empty x)
 ;;
@@ -113,7 +110,7 @@ let rec print_info_script sigma osign pf =
   match pf.ref with
     | None -> (mt ())
     | Some(r,spfl) ->
-        pr_rule r ++
+        Tactic_printer.pr_rule r ++
            match spfl with
              | [] ->
 		   (str " " ++ fnl())
@@ -152,8 +149,7 @@ let pp_string x =
 (***************************************************************************)
 
 let unify_e_resolve  (c,clenv) gls = 
-  let (wc,kONT) = startWalk gls in
-  let clenv' = connect_clenv wc clenv in
+  let clenv' = connect_clenv gls clenv in
   let _ = clenv_unique_resolver false clenv' gls in
   vernac_e_resolve_constr c gls
 
@@ -179,7 +175,7 @@ and e_my_find_search db_list local_db hdc concl =
       list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
   in 
   let tac_of_hint = 
-    fun ({pri=b; pat = p; code=t} as patac) -> 
+    fun ({pri=b; pat = p; code=t} as _patac) -> 
       (b, 
        let tac =
 	 match t with
@@ -189,7 +185,7 @@ and e_my_find_search db_list local_db hdc concl =
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve (term,cl)) 
 		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> unfold_constr c
+	   | Unfold_nth c -> unfold_in_concl [[],c]
 	   | Extern tacast -> Auto.conclPattern concl 
 	       (out_some p) tacast
        in 
@@ -341,7 +337,7 @@ let e_breadth_search debug n db_list local_db gl =
   with Not_found -> error "EAuto: breadth first search failed"
 
 let e_search_auto debug (n,p) db_list gl = 
-  let local_db = make_local_hint_db gl in 
+  let local_db = make_local_hint_db [] gl in 
   if n = 0 then 
     e_depth_search debug p db_list local_db gl
   else 
@@ -351,17 +347,17 @@ let eauto debug np dbnames =
   let db_list =
     List.map
       (fun x -> 
-	 try Stringmap.find x !searchtable
+	 try searchtable_map x
 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
   tclTRY (e_search_auto debug np db_list)
 
 let full_eauto debug n gl = 
-  let dbnames = stringmap_dom !searchtable in
+  let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
-  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
-  let local_db = make_local_hint_db gl in
+  let db_list = List.map searchtable_map dbnames in
+  let _local_db = make_local_hint_db [] gl in
   tclTRY (e_search_auto debug n db_list) gl
 
 let my_full_eauto n gl = full_eauto false (n,0) gl
@@ -369,8 +365,6 @@ let my_full_eauto n gl = full_eauto false (n,0) gl
 (**********************************************************************
    copié de tactics/auto.ml on a juste modifié search_gen
 *)
-let searchtable_map name = 
-  Stringmap.find name !searchtable
 
 (* local_db is a Hint database containing the hypotheses of current goal *)
 (* Papageno : cette fonction a été pas mal simplifiée depuis que la base
@@ -397,7 +391,7 @@ and my_find_search db_list local_db hdc concl =
       	(local_db::db_list)
   in
   List.map 
-    (fun ({pri=b; pat=p; code=t} as patac) -> 
+    (fun ({pri=b; pat=p; code=t} as _patac) -> 
        (b,
 	match t with
 	  | Res_pf (term,cl)  -> unify_resolve (term,cl)
@@ -407,7 +401,7 @@ and my_find_search db_list local_db hdc concl =
 	      tclTHEN 
 		(unify_resolve (term,cl)) 
 		(trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> unfold_constr c
+	  | Unfold_nth c -> unfold_in_concl [[],c]
 	  | Extern tacast -> 
 	      conclPattern concl (out_some p) tacast))
     tacl
@@ -476,7 +470,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   try 
 	     [make_apply_entry (pf_env g') (project g')
 		(true,false) 
-		hid (mkVar hid,body_of_type htyp)]
+		(mkVar hid,body_of_type htyp)]
 	   with Failure _ -> [] 
 	 in
          (free_try
@@ -499,11 +493,11 @@ let search = search_gen 0
 let default_search_depth = ref 5
 			     
 let full_auto n gl = 
-  let dbnames = stringmap_dom !searchtable in
+  let dbnames = current_db_names () in
   let dbnames = list_subtract dbnames ["v62"] in
-  let db_list = List.map (fun x -> searchtable_map x) dbnames in
+  let db_list = List.map searchtable_map dbnames in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db [] gl) hyps) gl
   
 let default_full_auto gl = full_auto !default_search_depth gl
 (************************************************************************)
@@ -568,7 +562,7 @@ let blast gls =
       open_subgoals = 1;
       goal = g;
       ref = None } in
-     try (let (sgl,v) as res = !blast_tactic gls in
+     try (let (sgl,v) as _res = !blast_tactic gls in
 	  let {it=lg} = sgl in
           if lg = [] 
           then (let pf = v (List.map leaf (sig_it sgl)) in
@@ -590,7 +584,7 @@ let blast gls =
 ;;
 
 let blast_tac display_function = function 
-          | (n::_) as l -> 
+          | (n::_) as _l -> 
                  (function g ->
                     let exp_ast = (blast g) in
                      (display_function exp_ast;
@@ -599,7 +593,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(Pptactic.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic x)));;
 
 (* Obsolète ?
 overwriting_add_tactic "Blast1" blast_tac_txt;;
diff --git a/contrib/interface/blast.mli b/contrib/interface/blast.mli
index 21c29bc9..f6701943 100644
--- a/contrib/interface/blast.mli
+++ b/contrib/interface/blast.mli
@@ -1,5 +1,3 @@
 val blast_tac : (Tacexpr.raw_tactic_expr -> 'a) ->
-    int list ->
-    Proof_type.goal Tacmach.sigma ->
-    Proof_type.goal list Proof_type.sigma * Proof_type.validation;;
+    int list -> Proof_type.tactic
 
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 7bf12f3b..8fcdb5d9 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.pr_lconstr 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.pr_lconstr 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
@@ -360,12 +342,13 @@ let debug_tac2_pcoq tac =
 	let the_ast = ref tac in
 	let the_path = ref ([] : int list) in
 	try
-	  let result = report_error tac the_goal the_ast the_path [] g in
+	  let _result = report_error tac the_goal the_ast the_path [] g in
 	  (errorlabstrm "DEBUG TACTIC"
-	     (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++
+	     (str "no error here " ++ fnl () ++ Printer.pr_goal (sig_it g) ++
 	      fnl () ++ str "the tactic is" ++ fnl () ++
-	      Pptactic.pr_glob_tactic tac);
-	   result)
+	      Pptactic.pr_glob_tactic (Global.env()) tac) (*
+Caution, this is in the middle of what looks like dead code. ;
+	   result *))
 	with
 	  e ->
 	    match !the_goal with
@@ -413,11 +396,11 @@ let inspect n =
 			 let (_, _, v) = get_variable (basename sp) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) v
 		     | (sp,kn), "CONSTANT" ->
-			 let {const_type=typ} = Global.lookup_constant kn in
+			 let {const_type=typ} = Global.lookup_constant (constant_of_kn kn) in
 			   add_search2 (Nametab.locate (qualid_of_sp sp)) typ
 		     | (sp,kn), "MUTUALINDUCTIVE" ->
 			 add_search2 (Nametab.locate (qualid_of_sp sp))
-			   (Pretyping.understand Evd.empty (Global.env())
+			   (Pretyping.Default.understand Evd.empty (Global.env())
 			      (RRef(dummy_loc, IndRef(kn,0))))
 		     | _ -> failwith ("unexpected value 1 for "^ 
 				      (string_of_id (basename (fst oname)))))
@@ -571,11 +554,11 @@ let pcoq_search s l =
 
 (* Check sequentially whether the pattern is one of the premises *)
 let rec hyp_pattern_filter pat name a c =
-  let c1 = strip_outer_cast c in
+  let _c1 = strip_outer_cast c in
     match kind_of_term c with
       | Prod(_, hyp, c2) -> 
 	  (try
-(*	     let _ = msgnl ((str "WHOLE ") ++ (Printer.prterm c)) in
+(*	     let _ = msgnl ((str "WHOLE ") ++ (Printer.pr_lconstr c)) in
              let _ = msgnl ((str "PAT ") ++ (Printer.pr_pattern pat)) in *)
              if Matching.is_matching pat hyp then
 	       (msgnl (str "ok"); true)
@@ -616,7 +599,7 @@ let pcoq_show_goal = function
   | Some n -> show_nth n
   | None ->
       if !pcoq_started = Some true (* = debug *) then
-	msg (Pfedit.pr_open_subgoals ())
+	msg (Printer.pr_open_subgoals ())
       else errorlabstrm "show_goal"
 	(str "Show must be followed by an integer in Centaur mode");;
 
@@ -632,17 +615,17 @@ let pcoq_hook = {
 }
 
 
-TACTIC EXTEND Pbp
-| [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> 
+TACTIC EXTEND pbp
+| [ "pbp" ident_opt(idopt) natural_list(nl) ] -> 
     [ if_pcoq pbp_tac_pcoq idopt nl ]
 END
 
-TACTIC EXTEND CtDebugTac
-| [ "DebugTac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
+TACTIC EXTEND ct_debugtac
+| [ "debugtac" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
 END
 
-TACTIC EXTEND CtDebugTac2
-| [ "DebugTac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
+TACTIC EXTEND ct_debugtac2
+| [ "debugtac2" tactic(t) ] -> [ if_pcoq debug_tac2_pcoq (fst t) ]
 END
 
 
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
deleted file mode 100644
index 67279bb8..00000000
--- 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 ec989296..578abc49 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 bf596b28..56abfb82 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 = Pptactic.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) ->
@@ -263,9 +239,14 @@ and checked_then: report_holder -> glob_tactic_expr -> glob_tactic_expr -> tacti
    by the list of integers given as extra arguments.
  *)
 
+let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
+let globwit_main_tactic = globwit_tactic Pcoq.Tactic.tactic_main_level
+let wit_main_tactic = wit_tactic Pcoq.Tactic.tactic_main_level
+
+
 let on_then = function [t1;t2;l] ->
-  let t1 = out_gen wit_tactic t1 in
-  let t2 = out_gen wit_tactic t2 in
+  let t1 = out_gen wit_main_tactic t1 in
+  let t2 = out_gen wit_main_tactic t2 in
   let l = out_gen (wit_list0 wit_int) l in
   tclTHEN_i (Tacinterp.eval_tactic t1)
     (fun i ->
@@ -276,78 +257,18 @@ let on_then = function [t1;t2;l] ->
   | _ -> anomaly "bad arguments for on_then";;
 
 let mkOnThen t1 t2 selected_indices =
-  let a = in_gen rawwit_tactic t1 in
-  let b = in_gen rawwit_tactic t2 in
+  let a = in_gen rawwit_main_tactic t1 in
+  let b = in_gen rawwit_main_tactic t2 in
   let l = in_gen (wit_list0 rawwit_int) selected_indices in
   TacAtom (dummy_loc, TacExtend (dummy_loc, "OnThen", [a;b;l]));;
 
 (* 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) ->
@@ -355,7 +276,7 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
 	  Report_node(true, n, l) -> tac
       	| Report_node(false, n, rl) ->
 	    TacThens (a,List.map2 reconstruct_success_tac l rl)
-      	| Failed n -> TacId ""
+      	| Failed n -> TacId []
       	| Tree_fail r -> reconstruct_success_tac a r
       	| Mismatch (n,p) -> a)
   | TacThen (a,b) ->
@@ -364,16 +285,16 @@ let rec reconstruct_success_tac (tac:glob_tactic_expr) =
 	| Report_node(false, n, rl) ->
 	    let selected_indices = select_success 1 rl in
 	    TacAtom (dummy_loc,TacExtend (dummy_loc,"OnThen",
-	      [in_gen globwit_tactic a;
-	       in_gen globwit_tactic b;
+	      [in_gen globwit_main_tactic a;
+	       in_gen globwit_main_tactic b;
 	       in_gen (wit_list0 globwit_int) selected_indices]))
-	| Failed n -> TacId ""
+	| Failed n -> TacId []
 	| 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) -> tac
-	| Failed n -> TacId ""
+	| Failed n -> TacId []
 	| _ ->
 	    errorlabstrm
 	      "this error case should not happen on an unknown tactic"
@@ -391,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 -> 
@@ -430,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 ->
@@ -554,8 +442,8 @@ let descr_first_error tac =
 	    (msgnl (str "Execution of this tactic raised message " ++ fnl () ++
 		    fnl () ++ Cerrors.explain_exn e ++ fnl () ++
 		    fnl () ++ str "on goal"  ++ fnl () ++
-		    pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++
-		    str "faulty tactic is" ++ fnl () ++ fnl () ++
+		    Printer.pr_goal (sig_it (strip_some !the_goal)) ++
+                    fnl () ++ str "faulty tactic is" ++ fnl () ++ fnl () ++
 		    pr_glob_tactic ((*flatten_then*) !the_ast) ++ fnl ());
 	     tclIDTAC g))
 
diff --git a/contrib/interface/debug_tac.mli b/contrib/interface/debug_tac.mli
index ded714b6..da4bbaa0 100644
--- a/contrib/interface/debug_tac.mli
+++ b/contrib/interface/debug_tac.mli
@@ -1,6 +1,6 @@
 
 val report_error : Tacexpr.glob_tactic_expr ->
-    Proof_type.goal Proof_type.sigma option ref ->
+    Proof_type.goal Evd.sigma option ref ->
     Tacexpr.glob_tactic_expr ref -> int list ref -> int list -> Tacmach.tactic;;
 
 val clean_path : Tacexpr.glob_tactic_expr -> int list -> int list;;
diff --git a/contrib/interface/line_parser.ml4 b/contrib/interface/line_parser.ml4
index b5669351..0b13a092 100755
--- a/contrib/interface/line_parser.ml4
+++ b/contrib/interface/line_parser.ml4
@@ -84,7 +84,7 @@ let rec string len = parser
    spaces and tabulations are ignored, identifiers, integers,
    strings, opening and closing square brackets.  Lexical errors are
    ignored ! *)
-let rec next_token = parser count
+let rec next_token = parser _count
   [< '' ' | '\t'; tok = next_token >] -> tok
 | [< ''_' | 'a'..'z' | 'A'..'Z' as c;i = (ident (add_in_buff 0 c))>] -> i
 | [< ''0'..'9' as c ; i = (parse_int (get_digit c))>] -> i
@@ -96,7 +96,7 @@ let rec next_token = parser count
 (* A very simple lexical analyser to recognize a integer value behind 
    blank characters *)
 
-let rec next_int = parser count
+let rec next_int = parser _count
   [< '' ' | '\t'; v = next_int >] -> v
 | [< ''0'..'9' as c; i = (parse_int (get_digit c))>] ->
      (match i with
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index eaff0968..b06ba199 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),
@@ -160,7 +140,7 @@ let make_variable_ast name typ implicits =
     
 
 let make_definition_ast name c typ implicits =
-  VernacDefinition ((Global,Definition), (dummy_loc,name), DefineBody ([], None,
+  VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
     (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
     (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
@@ -173,9 +153,9 @@ let constant_to_ast_list kn =
   let l = implicits_of_global (ConstRef kn) in
   (match c with
       None -> 
-	make_variable_ast (id_of_label (label kn)) typ l
+	make_variable_ast (id_of_label (con_label kn)) typ l
     | Some c1 ->
-	make_definition_ast (id_of_label (label kn)) (Declarations.force c1) typ l)
+	make_definition_ast (id_of_label (con_label kn)) (Declarations.force c1) typ l)
 
 let variable_to_ast_list sp =
   let (id, c, v) = get_variable sp in
@@ -198,7 +178,7 @@ let leaf_entry_to_ast_list ((sp,kn),lobj) =
   let tag = object_tag lobj in
   match tag with
   | "VARIABLE" -> variable_to_ast_list (basename sp)
-  | "CONSTANT" -> constant_to_ast_list kn
+  | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn)
   | "INDUCTIVE" -> inductive_to_ast_list kn
   | s -> 
       errorlabstrm 
@@ -240,7 +220,7 @@ let name_to_ast ref =
 		   | Some c1 -> make_definition_ast name c1 typ [])
 	  with Not_found ->
 	    try
-	      let sp = Nametab.locate_syntactic_definition qid in
+	      let _sp = Nametab.locate_syntactic_definition qid in
 		errorlabstrm "print"
       		  (str "printing of syntax definitions not implemented")
 	    with Not_found ->
diff --git a/contrib/interface/name_to_ast.mli b/contrib/interface/name_to_ast.mli
index 0eca0a1e..b8c2d7dc 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 3f0b2d2e..4d4df59f 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -48,55 +48,8 @@ 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
-  | VernacGrammar _ -> Vernacentries.interp v
   | VernacOpenCloseScope sc -> Vernacentries.interp v
   | VernacRequire (_,_,l) ->
       (try 
@@ -202,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))
@@ -216,27 +163,14 @@ 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
     match first_ast with
     | ParseOK (Some (loc,ast)) ->
-        let ast0 = (execute_when_necessary ast) in
+        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()
@@ -311,7 +245,7 @@ let parse_file_action reqid file_name =
         get the text when a syntax error occurs *)
      let file_chan_err = open_in file_name in 
      let stream = Stream.of_channel file_chan in
-     let stream_err = Stream.of_channel file_chan_err in
+     let _stream_err = Stream.of_channel file_chan_err in
      let rec discard_to_dot () =
        try Gram.Entry.parse parse_to_dot (Gram.parsable stream)
        with Stdpp.Exc_located(_,Token.Error _) -> discard_to_dot() in
@@ -345,7 +279,7 @@ let parse_file_action reqid file_name =
 		   
              with
                | ParseOK (Some (_,ast)) ->
-		   let ast0=(execute_when_necessary ast) in 
+		   let _ast0=(execute_when_necessary ast) in 
 		   let term =
                      (try xlate_vernac ast
 		      with e ->
@@ -395,13 +329,13 @@ let add_path_action reqid string_arg =
 
 let print_version_action () =
   msgnl (mt ());
-  msgnl (str "$Id: parse.ml,v 1.22 2004/04/21 08:36:58 barras Exp $");;
+  msgnl (str "$Id: parse.ml 7844 2006-01-11 16:36:14Z bertot $");;
 
 let load_syntax_action reqid module_name =
  msg (str "loading " ++ str module_name ++ str "... ");
  try
       (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in
-      read_library (dummy_loc,qid);
+      require_library [dummy_loc,qid] None;
       msg (str "opening... ");
       Declaremods.import_module false (Nametab.locate_module qid); 
       msgnl (str "done" ++ fnl ());
@@ -456,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 -> ()
@@ -470,7 +403,7 @@ Libobject.relax true;
 (try let user_vernacrc =
    try Some(Sys.getenv "USERVERNACRC")
    with
-     | Not_found as e ->
+     | Not_found ->
 	 msgnl (str "no .vernacrc file"); None in
    (match user_vernacrc with
       	Some f -> coqparser_loop (open_in f)
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index e0f88ba6..d2f71bfc 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -34,13 +34,13 @@ let get_hyp_by_name g name =
   let evd = project g in
   let env = pf_env g in
   try (let judgment = 
-         Pretyping.understand_judgment 
+         Pretyping.Default.understand_judgment 
           evd env (RVar(zz, name)) in
        ("hyp",judgment.uj_type))
 (* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
    Loïc *)
   with _ -> (let c = Nametab.global (Ident (zz,name)) in
-             ("cste",type_of (Global.env()) Evd.empty (constr_of_reference c)))
+             ("cste",type_of (Global.env()) Evd.empty (constr_of_global c)))
 ;;
 
 type pbp_atom =
@@ -106,7 +106,7 @@ let make_final_cmd f optname clear_names constr path =
     add_clear_names_if_necessary (f optname constr path) clear_names;;
 
 let (rem_cast:pbp_rule) = function
-    (a,c,cf,o, Cast(f,_), p, func) ->
+    (a,c,cf,o, Cast(f,_,_), p, func) ->
       Some(func a c cf o (kind_of_term f) p)
   | _ -> None;;
 
@@ -154,7 +154,7 @@ let make_pbp_pattern x =
      [make_var (id_of_string ("Value_for_" ^ (string_of_id x)))]
 
 let rec make_then = function
-  | [] -> TacId ""
+  | [] -> TacId []
   | [t] -> t
   | t1::t2::l -> make_then (TacThen (t1,t2)::l)
 
@@ -177,7 +177,7 @@ let make_pbp_atomic_tactic = function
       TacAtom
 	(zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None))
   | PbpTryClear l -> 
-      TacTry (TacAtom (zz, TacClear (List.map (fun s -> AI (zz,s)) l)))
+      TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l)))
   | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));;
 
 let rec make_pbp_tactic = function
@@ -203,7 +203,7 @@ let (imply_elim1: pbp_rule) = function
   Some h, Prod(Anonymous, prem, body), 1::path, f ->
   let clear_names' = if clear_flag then h::clear_names else clear_names in
   let h' = next_global_ident hyp_radix avoid in
-  let str_h' = (string_of_id h') in
+  let _str_h' = (string_of_id h') in
   Some(PbpThens
 	  ([PbpLApply h],
 	   [chain_tactics [make_named_intro h'] (make_clears (h::clear_names));
diff --git a/contrib/interface/pbp.mli b/contrib/interface/pbp.mli
index 43ec1274..9daba184 100644
--- a/contrib/interface/pbp.mli
+++ b/contrib/interface/pbp.mli
@@ -1,4 +1,2 @@
 val pbp_tac : (Tacexpr.raw_tactic_expr -> 'a) ->
-    Names.identifier option -> int list ->
-    Proof_type.goal Tacmach.sigma ->
-    Proof_type.goal list Proof_type.sigma * Proof_type.validation;;
+    Names.identifier option -> int list -> Proof_type.tactic
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 5b265ec8..b7da5c1b 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
@@ -54,7 +53,7 @@ and ngoal=
      {newhyp : nhyp list;
       t_concl : Term.constr;
       t_full_concl: Term.constr;
-      t_full_env: Sign.named_context}
+      t_full_env: Environ.named_context_val}
 and ntree=
       {t_info:string;
 	t_goal:ngoal;
@@ -151,7 +150,7 @@ let seq_to_lnhyp sign sign' cl =
       {newhyp=nh;
        t_concl=cl;
        t_full_concl=long_type_hyp !lh cl;
-       t_full_env = sign@sign'}
+       t_full_env = Environ.val_of_named_context (sign@sign')}
 ;;
 
 
@@ -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  *)
 
 
@@ -226,7 +197,7 @@ let fill_unproved nt l =
 let new_sign osign sign =
     let res=ref [] in
     List.iter (fun (id,c,ty) ->
-		   try (let  (_,_,ty1)= (lookup_named id osign) in
+		   try (let  (_,_,_ty1)= (lookup_named id osign) in
 			())
 		   with Not_found -> res:=(id,c,ty)::(!res))
               sign;
@@ -247,6 +218,7 @@ let old_sign osign sign =
 let  to_nproof sigma osign pf =
   let rec to_nproof_rec sigma osign pf =
     let {evar_hyps=sign;evar_concl=cl} = pf.goal in
+    let sign = Environ.named_context_of_val sign in
     let nsign = new_sign osign sign in 
     let oldsign = old_sign osign sign in 
     match pf.ref with
@@ -417,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
@@ -759,7 +724,7 @@ let rec nsortrec vl x =
           nsortrec vl (mkInd (inductive_of_constructor c))
    | Case(_,x,t,a) 
         -> nsortrec vl x
-   | Cast(x,t)-> nsortrec vl t
+   | Cast(x,_, t)-> nsortrec vl t
    | Const c  -> nsortrec vl (lookup_constant c vl).const_type
    | _ -> nsortrec vl (type_of vl Evd.empty x)
 ;;
@@ -791,7 +756,7 @@ let rec group_lhyp lh =
 let natural_ghyp (sort,ln,lt) intro =
   let t=List.hd lt in
   let nh=List.length ln in
-  let ns=List.hd ln in
+  let _ns=List.hd ln in
   match sort with
     Nprop -> soit_A_une_proposition nh ln t
   | Ntype -> soit_X_un_element_de_T nh ln t
@@ -963,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"
@@ -991,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}
@@ -1285,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
@@ -1294,7 +1206,7 @@ let rec natural_ntree ig ntree =
 	  | TacExact c -> natural_exact ig lh g gs c ltree
 	  | TacCut c -> natural_cut ig lh g gs c ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
-	      let c = out_gen wit_constr a in
+	      let _c = out_gen wit_constr a in
 	      natural_cutintro ig lh g gs a ltree
 	  | TacCase (c,_) -> natural_case ig lh g gs ge c ltree false
 	  | TacExtend (_,"CaseIntro",[a]) ->
@@ -1518,7 +1430,7 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
 	 if with_intros
          then (arity_of_constr_of_mind env indf 1)
 	 else 0 in
-       let ici= 1 in
+       let _ici= 1 in
        sph[ (natural_ntree  
                {ihsg=
                  (match (nsort targ1) with
@@ -1547,7 +1459,7 @@ and prod_list_var t =
 and  hd_is_mind t ti =
     try (let env = Global.env() in
          let IndType (indf,targ) = find_rectype env Evd.empty t in
-	 let ncti= Array.length(get_constructors env indf) in
+	 let _ncti= Array.length(get_constructors env indf) in
 	 let (ind,_) = dest_ind_family indf in
          let (mib,mip) = lookup_mind_specif env ind in
 	 (string_of_id mip.mind_typename) = ti)
@@ -1556,7 +1468,7 @@ and mind_ind_info_hyp_constr indf c =
   let env = Global.env() in
   let (ind,_) = dest_ind_family indf in
   let (mib,mip) = lookup_mind_specif env ind in
-  let p = mip.mind_nparams in
+  let _p = mib.mind_nparams in
   let a = arity_of_constr_of_mind env indf c in
   let lp=ref (get_constructors env indf).(c).cs_args in
   let lr=ref [] in
@@ -1586,8 +1498,8 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
  let ncti= Array.length(get_constructors env indf) in
  let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
- let ti =(string_of_id mip.mind_typename) in
- let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
+ let _ti =(string_of_id mip.mind_typename) in
+ let _type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
   spv
          [  (natural_lhyp lh ig.ihsg);
              (show_goal2 lh ig g gs "");
@@ -1630,11 +1542,11 @@ and natural_induction ig lh g gs ge arg2 ltree with_intros=
  let arg1= mkVar arg2 in
  let targ1 = prod_head (type_of env Evd.empty arg1) in
  let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors env indf) in
+ let _ncti= Array.length(get_constructors env indf) in
  let (ind,_) = dest_ind_family indf in
  let (mib,mip) = lookup_mind_specif env ind in
- let ti =(string_of_id mip.mind_typename) in
- let type_arg= targ1(*List.nth targ (mis_index dmi)*) in
+ let _ti =(string_of_id mip.mind_typename) in
+ let _type_arg= targ1(*List.nth targ (mis_index dmi)*) in
 
  let lh1= hyps (List.hd ltree) in (* la liste des hyp jusqu'a n *)
  (* on les enleve des hypotheses des sous-buts *)
@@ -1719,8 +1631,8 @@ and natural_reduce ig lh g gs ge mode la ltree =
 and natural_split ig lh g gs ge la ltree =
   match la with
     [arg] -> 
-      let env= (gLOB ge) in
-      let arg1= (*dbize env*) arg in
+      let _env= (gLOB ge) in
+      let arg1= (*dbize _env*) arg in
       spv
       	[ (natural_lhyp lh ig.ihsg);
           (show_goal2 lh ig g gs ""); 
@@ -1740,9 +1652,9 @@ and natural_split ig lh g gs ge la ltree =
 and natural_generalize ig lh g gs ge la ltree =
   match la with
     [arg] ->
-      let env= (gLOB ge) in
+      let _env= (gLOB ge) in
       let arg1= (*dbize env*) arg in
-      let type_arg=type_of (Global.env()) Evd.empty arg in
+      let _type_arg=type_of (Global.env()) Evd.empty arg in
 (*      let type_arg=type_of_ast ge arg in*)
       spv
       	[ (natural_lhyp lh ig.ihsg);
diff --git a/contrib/interface/showproof.mli b/contrib/interface/showproof.mli
index ee269458..9b6787b7 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 ee901c5e..dd7f455d 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
@@ -131,12 +130,12 @@ let rec sp_print x =
 	     | "\n" -> fnl ()
 	     | "Retour chariot pour Show proof" -> fnl ()
 	     |_ -> str s)
-     | CT_text_formula  f -> prterm (Hashtbl.find ct_FORMULA_constr f)
+     | CT_text_formula  f -> pr_lconstr (Hashtbl.find ct_FORMULA_constr f)
      | CT_text_op [CT_coerce_ID_to_TEXT (CT_ident "to_prove");
 		   CT_text_path (CT_signed_int_list p);
 		   CT_coerce_ID_to_TEXT (CT_ident "goal");
 		   g] ->
-      let p=(List.map (fun y -> match y with
+      let _p=(List.map (fun y -> match y with
 	                 (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
@@ -149,7 +148,7 @@ let rec sp_print x =
 	      CT_text_path (CT_signed_int_list p);
 	      CT_coerce_ID_to_TEXT (CT_ident hyp);
               g]  ->
-      let p=(List.map (fun y -> match y with
+      let _p=(List.map (fun y -> match y with
 	                  (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
@@ -159,7 +158,7 @@ let rec sp_print x =
 	      CT_text_path (CT_signed_int_list p);
 	      CT_coerce_ID_to_TEXT (CT_ident hyp);
               g]  ->
-      let p=(List.map (fun y -> match y with
+      let _p=(List.map (fun y -> match y with
                          (CT_coerce_INT_to_SIGNED_INT
 			      (CT_int x)) -> x
 		       | _ -> raise (Failure "sp_print")) p) in
diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index e63baecf..6e4782be 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/vernacrc b/contrib/interface/vernacrc
index 42b5e5ab..4d3dc558 100644
--- a/contrib/interface/vernacrc
+++ b/contrib/interface/vernacrc
@@ -1,4 +1,4 @@
-# $Id: vernacrc,v 1.3 2004/01/14 14:52:59 bertot Exp $
+# $Id: vernacrc 5202 2004-01-14 14:52:59Z bertot $
 
 # This file is loaded initially by ./vernacparser.
 
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index ff418523..5a7ccc26 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -407,6 +407,9 @@ and fCOMMAND = function
    fNODE "print_about" 1
 | CT_print_all -> fNODE "print_all" 0
 | CT_print_classes -> fNODE "print_classes" 0
+| CT_print_ltac id ->
+   fID id;
+   fNODE "print_ltac" 1
 | CT_print_coercions -> fNODE "print_coercions" 0
 | CT_print_grammar(x1) ->
    fGRAMMAR x1;
@@ -418,6 +421,9 @@ and fCOMMAND = function
 | CT_print_hintdb(x1) ->
    fID_OR_STAR x1;
    fNODE "print_hintdb" 1
+| CT_print_rewrite_hintdb(x1) ->
+   fID x1;
+   fNODE "print_rewrite_hintdb" 1
 | CT_print_id(x1) ->
    fID x1;
    fNODE "print_id" 1
@@ -451,6 +457,7 @@ and fCOMMAND = function
 | CT_print_scope(x1) ->
    fID x1;
    fNODE "print_scope" 1
+| CT_print_setoids -> fNODE "print_setoids" 0
 | CT_print_scopes -> fNODE "print_scopes" 0
 | CT_print_section(x1) ->
    fID x1;
@@ -1153,12 +1160,12 @@ and fMODULE_TYPE = function
 | CT_coerce_ID_to_MODULE_TYPE x -> fID x
 | CT_module_type_with_def(x1, x2, x3) ->
    fMODULE_TYPE x1;
-   fID x2;
+   fID_LIST x2;
    fFORMULA x3;
    fNODE "module_type_with_def" 3
 | CT_module_type_with_mod(x1, x2, x3) ->
    fMODULE_TYPE x1;
-   fID x2;
+   fID_LIST x2;
    fID x3;
    fNODE "module_type_with_mod" 3
 and fMODULE_TYPE_CHECK = function
@@ -1281,6 +1288,7 @@ and fRED_COM = function
    fPATTERN_NE_LIST x1;
    fNODE "pattern" 1
 | CT_red -> fNODE "red" 0
+| CT_cbvvm -> fNODE "vm_compute" 0
 | CT_simpl(x1) ->
    fPATTERN_OPT x1;
    fNODE "simpl" 1
@@ -1545,6 +1553,9 @@ and fTACTIC_COM = function
 | CT_exact(x1) ->
    fFORMULA x1;
    fNODE "exact" 1
+| CT_exact_no_check(x1) ->
+   fFORMULA x1;
+   fNODE "exact_no_check" 1
 | CT_exists(x1) ->
    fSPEC_LIST x1;
    fNODE "exists" 1
@@ -1649,12 +1660,12 @@ and fTACTIC_COM = function
    fID x2;
    fNODE "move_after" 2
 | CT_new_destruct(x1, x2, x3) ->
-   fFORMULA_OR_INT x1;
+   (List.iter fFORMULA_OR_INT x1); (* Julien F. Est-ce correct? *)
    fUSING x2;
    fINTRO_PATT_OPT x3;
    fNODE "new_destruct" 3
 | CT_new_induction(x1, x2, x3) ->
-   fFORMULA_OR_INT x1;
+   (List.iter fFORMULA_OR_INT x1); (* Pierre C. Est-ce correct? *)
    fUSING x2;
    fINTRO_PATT_OPT x3;
    fNODE "new_induction" 3
@@ -1697,10 +1708,12 @@ and fTACTIC_COM = function
 | CT_repeat(x1) ->
    fTACTIC_COM x1;
    fNODE "repeat" 1
-| CT_replace_with(x1, x2) ->
+| CT_replace_with(x1, x2,x3,x4) ->
    fFORMULA x1;
    fFORMULA x2;
-   fNODE "replace_with" 2
+   fID_OPT x3;
+   fTACTIC_OPT x4;
+   fNODE "replace_with" 4
 | CT_rewrite_lr(x1, x2, x3) ->
    fFORMULA x1;
    fSPEC_LIST x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 02dc57de..da87086e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -3,7 +3,6 @@
 open String;;
 open Char;;
 open Util;;
-open Ast;;
 open Names;;
 open Ascent;;
 open Genarg;;
@@ -64,11 +63,7 @@ let coercion_description t = !coercion_description_holder t;;
 let set_coercion_description f =
  coercion_description_holder:=f; ();;
 
-let string_of_node_loc the_node =
-  match Util.unloc (loc the_node) with
-      (a,b) -> "(" ^ (string_of_int a) ^ ", " ^ (string_of_int b) ^ ")";;
-
-let xlate_error s = failwith ("Translation error: " ^ s);;
+let xlate_error s = print_endline ("xlate_error : "^s);failwith ("Translation error: " ^ s);;
 
 let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;;
 
@@ -266,11 +261,13 @@ let rec xlate_match_pattern =
     | CPatAlias  (_,  pattern, id) ->
      CT_pattern_as
       (xlate_match_pattern pattern, CT_coerce_ID_to_ID_OPT (xlate_ident id))
+    | CPatOr (_,l) -> xlate_error "CPatOr: TODO"
     | CPatDelimiters(_, key, p) -> 
 	CT_pattern_delimitors(CT_num_type key, xlate_match_pattern p)
-    | CPatNumeral(_,n) ->
+    | CPatPrim (_,Numeral n) ->
  	CT_coerce_NUM_to_MATCH_PATTERN
-	  (CT_int_encapsulator(Bignat.bigint_to_string n))
+	  (CT_int_encapsulator(Bigint.to_string n))
+    | CPatPrim (_,String _) -> xlate_error "CPatPrim (String): TODO"
     | CPatNotation(_, s, l) -> 
 	CT_pattern_notation(CT_string s,
 			    CT_match_pattern_list(List.map xlate_match_pattern l))
@@ -373,14 +370,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),
@@ -393,27 +387,18 @@ 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) -> 
-       let case_string = match c with
-	   Term.MatchStyle -> "Match"
-	 | _ -> "Case" in
-	 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) -> 
-       CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bignat.bigint_to_string i))
+   | CPrim (_, Numeral i) -> 
+       CT_coerce_NUM_to_FORMULA(CT_int_encapsulator(Bigint.to_string i))
+   | CPrim (_, String _) -> xlate_error "CPrim (String): TODO"
    | CHole _ -> CT_existvarc 
 (* I assume CDynamic has been inserted to make free form extension of
    the language possible, but this would go agains the logic of pcoq anyway. *)
    | CDynamic (_, _) -> assert false
    | CDelimiters (_, key, num) -> 
 	 CT_num_encapsulator(CT_num_type key , xlate_formula  num)
-   | CCast (_, e, t) -> 
+   | CCast (_, e,_, t) -> 
        CT_coerce_TYPED_FORMULA_to_FORMULA
 	 (CT_typed_formula(xlate_formula e, xlate_formula t))
    | CPatVar (_, (_,i)) when is_int_meta i ->
@@ -430,11 +415,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
         CT_cofixc(xlate_ident id,
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi)))
    | CFix (_, (_, id), lm::lmi) ->       
-     let strip_mutrec (fid, n, bl, arf, ardef) =
+     let strip_mutrec (fid, (n, ro), 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
            (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
@@ -485,14 +469,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)))
@@ -631,6 +615,7 @@ let rec xlate_intro_pattern =
 	   ll)
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
+  | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
 
 let compute_INV_TYPE = function
    FullInversionClear -> CT_inv_clear
@@ -678,9 +663,11 @@ let xlate_one_unfold_block = function
   | (n::nums, qid) ->
       CT_unfold_occ(tac_qualid_to_ct_ID qid, nums_to_int_ne_list n nums);;
 
-let xlate_intro_patt_opt = function
-    None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
-  | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+let xlate_with_names = function
+    IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
+  | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+
+let rawwit_main_tactic = rawwit_tactic Pcoq.Tactic.tactic_main_level
 
 let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
   function
@@ -729,6 +716,7 @@ and xlate_red_tactic =
  function
   | Red true -> xlate_error ""
   | Red false -> CT_red
+  | CbvVm -> CT_cbvvm
   | Hnf -> CT_hnf
   | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
   | Simpl (Some (l,c)) -> 
@@ -788,6 +776,7 @@ and xlate_tactic =
    | TacFirst(t1::l)-> CT_first(xlate_tactic t1, List.map xlate_tactic l)
    | TacSolve([]) -> assert false
    | TacSolve(t1::l)-> CT_tacsolve(xlate_tactic t1, List.map xlate_tactic l)
+   | TacComplete _ -> xlate_error "TODO: tactical complete"
    | TacDo(count, t) -> CT_do(xlate_id_or_int count, xlate_tactic t)
    | TacTry t -> CT_try (xlate_tactic t)
    | TacRepeat t -> CT_repeat(xlate_tactic t)
@@ -798,7 +787,8 @@ and xlate_tactic =
 		   xlate_tactic t)
    | TacProgress t -> CT_progress(xlate_tactic t)
    | TacOrelse(t1,t2) -> CT_orelse(xlate_tactic t1, xlate_tactic t2)
-   | TacMatch (exp, rules) ->
+   | TacMatch (true,_,_) -> failwith "TODO: lazy match"
+   | TacMatch (false, exp, rules) ->
         CT_match_tac(xlate_tactic exp,
                      match List.map 
                        (function 
@@ -814,11 +804,11 @@ and xlate_tactic =
                          | [] -> assert false
                          | fst::others ->
                              CT_match_tac_rules(fst, others))
-   | TacMatchContext (_,[]) -> failwith ""
-   | TacMatchContext (false,rule1::rules) ->
+   | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
+   | TacMatchContext (false,false,rule1::rules) ->
          CT_match_context(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacMatchContext (true,rule1::rules) ->
+   | TacMatchContext (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
    | TacLetIn (l, t) ->
@@ -855,18 +845,23 @@ and xlate_tactic =
 		   (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
        CT_rec_tactic_in(tl, xlate_tactic t)
    | TacAtom (_, t) -> xlate_tac t 
-   | TacFail (count, "") -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
-   | TacFail (count, s) -> CT_fail(xlate_id_or_int count,
+   | TacFail (count, []) -> CT_fail(xlate_id_or_int count, ctf_STRING_OPT_NONE)
+   | TacFail (count, [MsgString s]) -> CT_fail(xlate_id_or_int count,
 				   ctf_STRING_OPT_SOME (CT_string s))
-   | TacId "" -> CT_idtac ctf_STRING_OPT_NONE
-   | TacId s -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
+   | TacFail (count, _) -> xlate_error "TODO: generic fail message"
+   | TacId [] -> CT_idtac ctf_STRING_OPT_NONE
+   | TacId [MsgString s] -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
+   | TacId _ -> xlate_error "TODO: generic idtac message"
    | TacInfo t -> CT_info(xlate_tactic t)
    | TacArg a -> xlate_call_or_tacarg a
 
 and xlate_tac =
   function
     | TacExtend (_, "firstorder", tac_opt::l) ->
-       let t1 = match out_gen (wit_opt rawwit_tactic) tac_opt with
+       let t1 =
+	 match
+	   out_gen (wit_opt rawwit_main_tactic) tac_opt
+	 with
 	 | None -> CT_coerce_NONE_to_TACTIC_OPT CT_none
 	 | Some t2 -> CT_coerce_TACTIC_COM_to_TACTIC_OPT (xlate_tactic t2) in
 	 (match l with
@@ -914,7 +909,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
@@ -962,53 +957,68 @@ and xlate_tac =
     | TacRight bindl -> CT_right (xlate_bindings bindl)
     | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl)
     | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl)
-    | TacExtend (_,"replace", [c1; c2]) ->
-     let c1 = xlate_formula (out_gen rawwit_constr c1) in
-     let c2 = xlate_formula (out_gen rawwit_constr c2) in
-     CT_replace_with (c1, c2)
+    | TacExtend (_,"replace", [c1; c2;id_opt;tac_opt]) ->
+	let c1 = xlate_formula (out_gen rawwit_constr c1) in
+	let c2 = xlate_formula (out_gen rawwit_constr c2) in
+	let id_opt = 
+	  match out_gen Extratactics.rawwit_in_arg_hyp id_opt with 
+	  | None -> ctv_ID_OPT_NONE
+	  | Some id ->   ctf_ID_OPT_SOME (xlate_ident id)
+	in
+	let tac_opt = 
+	  match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with
+	    | None -> CT_coerce_NONE_to_TACTIC_OPT  CT_none
+	    | Some tac ->
+		let tac =  xlate_tactic tac in
+		CT_coerce_TACTIC_COM_to_TACTIC_OPT tac
+	in 
+	CT_replace_with (c1, c2,id_opt,tac_opt)
     | TacExtend (_,"rewrite", [b; cbindl]) ->
      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_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]) ->
-     let t = out_gen rawwit_tactic t in
+    | 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 (_,"conditionalrewritein", [t; b; cbindl; id]) ->
-     let t = out_gen rawwit_tactic t in
+    | 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; id_or_constr]) ->
+    | TacExtend (_,"dependent_rewrite", [b; c]) ->
       let b = out_gen Extraargs.rawwit_orient b in
-      (match genarg_tag id_or_constr with
-	| IdentArgType -> (*Dependent Rewrite/SubstHypInConcl*)
-	    let id = xlate_ident (out_gen rawwit_ident id_or_constr) 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
-	| ConstrArgType -> (*CutRewrite/SubstConcl*)
-	    let c = xlate_formula (out_gen rawwit_constr id_or_constr) in
-	    if b then CT_cutrewrite_lr (c, ctv_ID_OPT_NONE)
-	    else CT_cutrewrite_rl (c, ctv_ID_OPT_NONE)
-	| _ -> xlate_error "")
-    | TacExtend (_,"dependentrewrite", [b; c; id]) -> (*CutRewrite in/SubstHyp*)
+	| _ -> xlate_error "dependent rewrite on term: not supported")
+    | TacExtend (_,"dependent_rewrite", [b; c; id]) ->
+	xlate_error "dependent rewrite on terms in hypothesis: not supported"
+    | 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 (_,"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]) ->
@@ -1021,6 +1031,7 @@ and xlate_tac =
     | TacTransitivity c -> CT_transitivity (xlate_formula c)
     | TacAssumption -> CT_assumption
     | TacExact c -> CT_exact (xlate_formula c)
+    | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c)
     | TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id)
     | TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id)
     | TacDestructConcl -> CT_dconcl
@@ -1031,14 +1042,16 @@ and xlate_tac =
         (if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none),
         (if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none))
     | TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
-    | TacAuto (nopt, Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
-    | TacAuto (nopt, None) ->
+    | TacAuto (nopt, [], Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
+    | TacAuto (nopt, [], None) ->
  	CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt,
 		      CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
-    | TacAuto (nopt, Some (id1::idl)) ->
+    | TacAuto (nopt, [], Some (id1::idl)) ->
 	CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt,
              CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
              CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
+    | TacAuto (nopt, _::_, _) ->
+	xlate_error "TODO: auto using"
     |TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) ->
        let (id_list:ct_ID list) =
 	 List.map (fun x -> CT_ident x) (out_gen (wit_list1 rawwit_pre_ident) l) in
@@ -1048,11 +1061,11 @@ and xlate_tac =
 	 match t with
 	     [t0] -> 
 	       CT_coerce_TACTIC_COM_to_TACTIC_OPT
-		 (xlate_tactic(out_gen rawwit_tactic t0))
+	       (xlate_tactic(out_gen rawwit_main_tactic t0))
 	   | [] -> CT_coerce_NONE_to_TACTIC_OPT CT_none
 	   | _ -> assert false in
 	 CT_autorewrite (CT_id_ne_list(fst, id_list1), t1)
-    | TacExtend (_,"eauto", [nopt; popt; idl]) ->
+    | TacExtend (_,"eauto", [nopt; popt; lems; idl]) ->
 	let first_n =
 	  match out_gen (wit_opt rawwit_int_or_var) nopt with
 	    | Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
@@ -1063,6 +1076,10 @@ and xlate_tac =
 	    | Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
 	    | Some ArgArg n -> xlate_int_to_id_or_int_opt n
 	    | None -> none_in_id_or_int_opt in
+	let _lems =
+	  match out_gen Eauto.rawwit_auto_using lems with
+	    | [] -> []
+	    | _ -> xlate_error "TODO: eauto using" in
 	let idl = out_gen Eauto.rawwit_hintbases idl in
           (match idl with
 	    None -> CT_eauto_with(first_n,
@@ -1084,12 +1101,14 @@ and xlate_tac =
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_formula c and bindl = xlate_bindings bindl in
      CT_eapply (c, bindl)
-    | TacTrivial (Some []) -> CT_trivial
-    | TacTrivial None -> 
+    | TacTrivial ([],Some []) -> CT_trivial
+    | TacTrivial ([],None) -> 
 	CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
-    | TacTrivial (Some (id1::idl)) ->
+    | TacTrivial ([],Some (id1::idl)) ->
 	 CT_trivial_with(CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
             (CT_id_ne_list(CT_ident id1,List.map (fun x -> CT_ident x) idl))))
+    | TacTrivial (_::_,_) ->
+	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
     | TacApply (c,bindl) ->
@@ -1111,7 +1130,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)
@@ -1123,20 +1142,21 @@ and xlate_tac =
         CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c)
     | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c)
     | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c)
-    | TacClear [] ->
+    | TacClear (false,[]) ->
 	xlate_error "Clear expects a non empty list of identifiers"
-    | TacClear (id::idl) ->
+    | TacClear (false,id::idl) ->
        let idl' = List.map xlate_hyp idl in
        CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
+    | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'"
     | (*For translating tactics/Inv.v *)
       TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
 	CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
-		     xlate_intro_patt_opt l,
+		     xlate_with_names l,
 	             CT_id_list (List.map xlate_hyp idl))
     | TacInversion (DepInversion (k,copt,l),quant_hyp) ->
 	let id = xlate_quantified_hypothesis quant_hyp in
 	CT_depinversion (compute_INV_TYPE k, id, 
-			 xlate_intro_patt_opt l, xlate_formula_opt copt)
+			 xlate_with_names l, xlate_formula_opt copt)
     | TacInversion (InversionUsing (c,idlist), id) ->
 	let id = xlate_quantified_hypothesis id in
 	  CT_use_inversion (id, xlate_formula c,
@@ -1148,28 +1168,34 @@ 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,_)) ->
-	CT_new_destruct
-	  (xlate_int_or_constr a, xlate_using b, 
-	   xlate_intro_patt_opt c)
-    | TacNewInduction(a,b,(c,_)) ->
-	CT_new_induction
-	  (xlate_int_or_constr a, xlate_using b,
-	   xlate_intro_patt_opt c)
-    | TacInstantiate (a, b, cl) -> 
+    | TacNewDestruct(a,b,c) ->
+	CT_new_destruct (* Julien F. : est-ce correct *)
+	  (List.map  xlate_int_or_constr a, xlate_using b, 
+	   xlate_with_names c)
+    | TacNewInduction(a,b,c) ->
+	CT_new_induction (* Pierre C. : est-ce correct *)
+	  (List.map xlate_int_or_constr a, xlate_using b,
+	   xlate_with_names c)
+    (*| TacInstantiate (a, b, cl) -> 
         CT_instantiate(CT_int a, xlate_formula b,
-		       xlate_clause cl)
+		       assert false) *)
+    | TacLetTac (na, c, cl) when cl = nowhere -> 
+        CT_pose(xlate_id_opt_aux na, xlate_formula c)
     | TacLetTac (na, c, cl) ->
         CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
 		     but the structures are different *)
 		  xlate_clause cl)
-    | TacForward (true, name, c) -> 
-               CT_pose(xlate_id_opt_aux name, xlate_formula c)
-    | TacForward (false, name, c) -> 
-               CT_assert(xlate_id_opt ((0,0),name), xlate_formula c)
-    | TacTrueCut (na, c) -> 
-        CT_truecut(xlate_id_opt ((0,0),na), xlate_formula c)
+    | TacAssert (None, IntroIdentifier id, c) -> 
+        CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
+    | TacAssert (None, IntroAnonymous, c) -> 
+        CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+    | TacAssert (Some (TacId []), IntroIdentifier id, c) -> 
+        CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
+    | TacAssert (Some (TacId []), IntroAnonymous, c) -> 
+        CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
+    | TacAssert _ ->
+	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
     | TacAnyConstructor(Some tac) -> 
 	CT_any_constructor
 	(CT_coerce_TACTIC_COM_to_TACTIC_OPT(xlate_tactic tac))
@@ -1181,6 +1207,7 @@ and xlate_tac =
 	     (List.map xlate_formula
 		(out_gen (wit_list0 rawwit_constr) args)))
     | TacExtend (_,id, l) ->
+	print_endline ("Extratactics : "^ id);
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
     | TacAlias _ -> xlate_error "Alias not supported"
 
@@ -1216,8 +1243,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
@@ -1233,19 +1263,14 @@ and coerce_genarg_to_TARG x =
       (CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x)))
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
-  | TacticArgType ->
-      let t = xlate_tactic (out_gen rawwit_tactic x) in
+  | TacticArgType n ->
+      let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
       CT_coerce_TACTIC_COM_to_TARG t
-  | OpenConstrArgType ->
-      CT_coerce_SCOMMENT_CONTENT_to_TARG
-      	(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
-						 (snd (out_gen
-						    rawwit_open_constr x))))
-  | CastedOpenConstrArgType -> 
+  | OpenConstrArgType b -> 
       CT_coerce_SCOMMENT_CONTENT_to_TARG
       	(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
-						 (snd (out_gen
-						    rawwit_casted_open_constr x))))
+					 (snd (out_gen
+					    (rawwit_open_constr_gen b) x))))
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
   | BindingsArgType -> xlate_error "TODO: generic with bindings"
   | RedExprArgType -> xlate_error "TODO: generic red expr"
@@ -1315,8 +1340,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
@@ -1332,11 +1360,10 @@ let coerce_genarg_to_VARG x =
       (CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula (out_gen rawwit_constr x)))
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
-  | TacticArgType ->
-      let t = xlate_tactic (out_gen rawwit_tactic x) in
+  | TacticArgType n ->
+      let t = xlate_tactic (out_gen (rawwit_tactic n) x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
-  | OpenConstrArgType -> xlate_error "TODO: generic open constr"
-  | CastedOpenConstrArgType -> xlate_error "TODO: generic open constr"
+  | OpenConstrArgType _ -> xlate_error "TODO: generic open constr"
   | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
   | BindingsArgType -> xlate_error "TODO: generic with bindings"
   | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
@@ -1347,23 +1374,9 @@ let coerce_genarg_to_VARG x =
   | ExtraArgType s -> xlate_error "Cannot treat extra generic arguments"
 
 
-let xlate_thm x = CT_thm (match x with
-  | Theorem -> "Theorem"
-  | Remark -> "Remark"
-  | Lemma -> "Lemma"
-  | Fact -> "Fact")
+let xlate_thm x = CT_thm (string_of_theorem_kind x)
 
-
-let xlate_defn x = CT_defn (match x with
- | (Local, Definition) -> "Local"
- | (Global, Definition) -> "Definition"
- | (Global, SubClass) -> "SubClass"
- | (Global, Coercion) -> "Coercion"
- | (Local, SubClass) -> "Local SubClass"
- | (Local, Coercion) -> "Local Coercion"
- | (Global,CanonicalStructure) -> "Canonical Structure"
- | (Local, CanonicalStructure) -> 
-     xlate_error "Local CanonicalStructure not parsed")
+let xlate_defn k = CT_defn (string_of_definition_kind k)
 
 let xlate_var x = CT_var (match x with
  | (Global,Definitional) -> "Parameter"
@@ -1511,17 +1524,18 @@ let rec xlate_module_type = function
   | CMTEwith(mty, decl) ->
       let mty1 = xlate_module_type mty in
 	(match decl with
-	     CWith_Definition((_, id), c) ->
-	       CT_module_type_with_def(xlate_module_type mty, 
-				       xlate_ident id, xlate_formula c)
-	   | CWith_Module((_, id), (_, qid)) ->
-	       CT_module_type_with_mod(xlate_module_type mty,
-				       xlate_ident id, 
+	     CWith_Definition((_, idl), c) ->
+	       CT_module_type_with_def(mty1, 
+				       CT_id_list (List.map xlate_ident idl),
+                                       xlate_formula c)
+	   | CWith_Module((_, idl), (_, qid)) ->
+	       CT_module_type_with_mod(mty1,
+				       CT_id_list (List.map xlate_ident idl), 
 				       CT_ident (xlate_qualid qid)));;
 
 let xlate_module_binder_list (l:module_binder list) =
   CT_module_binder_list
-    (List.map (fun (idl, mty) ->
+    (List.map (fun (_, idl, mty) ->
 		 let idl1 = 
 		   List.map (fun (_, x) -> CT_ident (string_of_id x)) idl in
 		 let fst,idl2 = match idl1 with
@@ -1643,18 +1657,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_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
@@ -1665,7 +1674,7 @@ let rec xlate_vernac =
   | VernacHints (local,dbnames,h) ->
       let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
       (match h with
-	| HintsConstructors (None, l) ->
+	| HintsConstructors l ->
 	 let n1, names = match List.map tac_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
@@ -1675,15 +1684,10 @@ let rec xlate_vernac =
 	   else
 	     CT_hints(CT_ident "Constructors",
 		      CT_id_ne_list(n1, names), dblist)
-	| HintsExtern (None, n, c, t) ->
+	| HintsExtern (n, c, t) ->
 	    CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
         | HintsResolve l | HintsImmediate l -> 
-	    let l = 
-	      List.map 
-	     	(function (None, f) -> xlate_formula f
-		   | _ -> 
-		       xlate_error "obsolete Hint Resolve not supported") l in
-	 let f1, formulas = match l  with
+	 let f1, formulas = match List.map xlate_formula l with
 	     a :: tl -> a, tl
 	   | _  -> failwith "" in
 	 let l' = CT_formula_ne_list(f1, formulas) in
@@ -1700,10 +1704,7 @@ let rec xlate_vernac =
 		| HintsImmediate _ -> CT_hints_immediate(l', dblist)
 		| _ -> assert false)
         | HintsUnfold l -> 
-	 let l = List.map
-	   (function (None,ref) -> loc_qualid_to_ct_ID ref |
-	      _ -> xlate_error "obsolete Hint Unfold not supported") l in
-	 let n1, names = match l with
+	 let n1, names = match List.map loc_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
 	   if local then
@@ -1724,9 +1725,6 @@ let rec xlate_vernac =
 	       CT_hint_destruct
 		 (xlate_ident id, CT_int n, dl, xlate_formula f,
 		  xlate_tactic t, dblist)
-	| HintsExtern(Some _, _, _, _)
-	| HintsConstructors(Some _, _) -> 
-            xlate_error "obsolete Hint Constructors not supported"
 )
   | VernacEndProof (Proved (true,None)) ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
@@ -1759,6 +1757,7 @@ let rec xlate_vernac =
   | VernacShow (ShowGoalImplicitly (Some n)) -> CT_show_implicit (CT_int n)
   | VernacShow ShowExistentials -> CT_show_existentials
   | VernacShow ShowScript -> CT_show_script
+  | VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)"
   | VernacGo arg -> CT_go (xlate_locn arg)
   | VernacShow ExplainProof l -> CT_explain_proof (nums_to_int_list l)
   | VernacShow ExplainTree l ->
@@ -1775,6 +1774,8 @@ let rec xlate_vernac =
 	| PrintHintDb -> CT_print_hintdb (CT_coerce_STAR_to_ID_OR_STAR CT_star)
 	| PrintHintDbName id -> 
 	    CT_print_hintdb (CT_coerce_ID_to_ID_OR_STAR (CT_ident id))
+	| PrintRewriteHintDbName id -> 
+	    CT_print_rewrite_hintdb (CT_ident id)
 	| PrintHint id ->
 	    CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
 	| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
@@ -1783,12 +1784,15 @@ let rec xlate_vernac =
 	| PrintMLModules -> CT_ml_print_modules
 	| PrintGraph -> CT_print_graph
 	| PrintClasses -> CT_print_classes
+	| PrintLtac qid -> CT_print_ltac (loc_qualid_to_ct_ID qid)
 	| PrintCoercions -> CT_print_coercions
 	| PrintCoercionPaths (id1, id2) -> 
 	    CT_print_path (xlate_class id1, xlate_class id2)
+	| PrintCanonicalConversions ->
+	    xlate_error "TODO: Print Canonical Structures"
 	| PrintInspect n -> CT_inspect (CT_int n)
 	| PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s)
-	| PrintLocalContext -> CT_print
+	| PrintSetoids -> CT_print_setoids
 	| PrintTables -> CT_print_tables
         | PrintModuleType a -> CT_print_module_type (loc_qualid_to_ct_ID a)
         | PrintModule a -> CT_print_module (loc_qualid_to_ct_ID a)
@@ -1867,13 +1871,12 @@ let rec xlate_vernac =
 	     translate_opt_notation_decl notopt) in
         CT_mind_decl
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
-   | VernacFixpoint [] -> xlate_error "mutual recursive"
-   | VernacFixpoint (lm :: lmi) ->
-      let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
+   | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
+   | VernacFixpoint ((lm :: lmi),boxed) ->
+      let strip_mutrec ((fid, (n, ro), 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
            (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
@@ -1885,8 +1888,8 @@ let rec xlate_vernac =
           | _ -> xlate_error "mutual recursive" in
         CT_fix_decl
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
-   | VernacCoFixpoint [] -> xlate_error "mutual corecursive"
-   | VernacCoFixpoint (lm :: lmi) ->
+   | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
+   | VernacCoFixpoint ((lm :: lmi),boxed) ->
       let strip_mutcorec (fid, bl, arf, ardef) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       xlate_formula arf, xlate_formula ardef) in
@@ -1916,20 +1919,18 @@ let rec xlate_vernac =
 			    | Some mty1 ->
 				CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT
 				  (xlate_module_type mty1))
-   | VernacDefineModule((_, id), bl, mty_o, mexpr_o) ->
+   | VernacDefineModule(_,(_, id), bl, mty_o, mexpr_o) ->
        CT_module(xlate_ident id, 
 		 xlate_module_binder_list bl,
 		 xlate_module_type_check_opt mty_o,
 		 match mexpr_o with
 		     None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
 		   | Some m -> xlate_module_expr m)
-  | VernacDeclareModule((_, id), bl, mty_o, mexpr_o) -> 
+  | VernacDeclareModule(_,(_, id), bl, mty_o) -> 
        CT_declare_module(xlate_ident id, 
 		 xlate_module_binder_list bl,
-		 xlate_module_type_check_opt mty_o,
-		 match mexpr_o with
-		     None -> CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE
-		   | Some m -> xlate_module_expr m)
+		 xlate_module_type_check_opt (Some mty_o),
+		 CT_coerce_ID_OPT_to_MODULE_EXPR ctv_ID_OPT_NONE)
    | VernacRequire (impexp, spec, id::idl) ->
       let ct_impexp, ct_spec = get_require_flags impexp spec in
       CT_require (ct_impexp, ct_spec, 
@@ -1943,8 +1944,6 @@ let rec xlate_vernac =
       CT_require(ct_impexp, ct_spec, 
 		 CT_coerce_STRING_to_ID_NE_LIST_OR_STRING(CT_string filename))
 
-   | VernacSyntax (phylum, l) -> xlate_error "SYNTAX not implemented"
-
    | VernacOpenCloseScope(true, true, s) -> CT_local_open_scope(CT_ident s)
    | VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s)
    | VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s)
@@ -1966,8 +1965,7 @@ let rec xlate_vernac =
 		     CT_id_ne_list(xlate_class_rawexpr a,
 				   List.map xlate_class_rawexpr l))
    | VernacBindScope(id, []) -> assert false
-   | VernacNotation(b, c, None, _, _) -> assert false
-   | VernacNotation(b, c, Some(s,modif_list), _, opt_scope) -> 
+   | VernacNotation(b, c, (s,modif_list), opt_scope) -> 
        let translated_s = CT_string s in
        let formula = xlate_formula c in
        let translated_modif_list = 
@@ -1981,7 +1979,7 @@ let rec xlate_vernac =
        else
 	 CT_define_notation(translated_s, formula, 
 			    translated_modif_list, translated_scope)
-   | VernacSyntaxExtension(b,Some(s,modif_list), None) -> 
+   | VernacSyntaxExtension(b,(s,modif_list)) -> 
        let translated_s = CT_string s in
        let translated_modif_list = 
 	 CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
@@ -1989,8 +1987,7 @@ let rec xlate_vernac =
 	 CT_local_reserve_notation(translated_s, translated_modif_list)
        else
 	 CT_reserve_notation(translated_s, translated_modif_list)
-   | VernacSyntaxExtension(_, _, _) -> assert false
-   | VernacInfix (b,(str,modl),id,_, opt_scope) ->
+   | VernacInfix (b,(str,modl),id, opt_scope) ->
        let id1 = loc_qualid_to_ct_ID id in
        let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in
        let s = CT_string str in
@@ -2001,7 +1998,6 @@ let rec xlate_vernac =
 	   CT_local_infix(s, id1,modl1, translated_scope)
 	 else
 	   CT_infix(s, id1,modl1, translated_scope)
-   | VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
    | VernacCoercion (s, id1, id2, id3) ->
       let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
       let local_opt =
@@ -2032,8 +2028,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))
@@ -2057,6 +2051,7 @@ let rec xlate_vernac =
   | VernacReserve([], _) -> assert false
   | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
   | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
+  | VernacLocate(LocateModule _) -> xlate_error "TODO: Locate Module"
   | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
   | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
   | VernacTime(v) -> CT_time(xlate_vernac v)
@@ -2113,9 +2108,9 @@ let rec xlate_vernac =
   | VernacVar _ -> xlate_error "Grammar vernac obsolete"
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)
-  | VernacBack _|VernacRestoreState _| VernacWriteState _|
-    VernacSolveExistential (_, _)|VernacCanonical _ | VernacDistfix _|
-     VernacTacticGrammar _)
+  | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
+    VernacSolveExistential (_, _)|VernacCanonical _ |
+     VernacTacticNotation _)
     -> xlate_error "TODO: vernac";;
 
 let rec xlate_vernac_list =
@@ -2123,8 +2118,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";;