Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)

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

18 files changed, 205 insertions, 492 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index e6d1194a5..e8faf862f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -205,12 +205,8 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
         in 
 	if eapply & (nmiss <> 0) then begin
           if verbose then 
-	    if !Options.v7 then
-	    warn (str "the hint: EApply " ++ prterm c ++
-		    str " will only be used by EAuto")
-	    else
 	    warn (str "the hint: eapply " ++ prterm c ++
-		    str " will only be used by eauto"); 
+		  str " will only be used by eauto"); 
           (hd,
            { hname = name;
 	     pri = nb_hyp cty + nmiss;
@@ -388,9 +384,6 @@ let add_unfolds l local dbnames =
 let add_extern name pri (patmetas,pat) tacast local dbname =
   (* We check that all metas that appear in tacast have at least
      one occurence in the left pattern pat *)
-(* TODO
-  let tacmetas = Coqast.collect_metas tacast in
-*)
   let tacmetas = [] in
   match (list_subtract tacmetas patmetas) with
     | i::_ ->
@@ -482,16 +475,6 @@ let add_hints local dbnames0 h =
 (**************************************************************************)
 
 let fmt_autotactic =
-  if !Options.v7 then
-  function
-  | Res_pf (c,clenv) -> (str"Apply " ++ prterm c)
-  | ERes_pf (c,clenv) -> (str"EApply " ++ prterm c)
-  | Give_exact c -> (str"Exact " ++ prterm c)
-  | Res_pf_THEN_trivial_fail (c,clenv) -> 
-      (str"Apply " ++ prterm c ++ str" ; Trivial")
-  | Unfold_nth c -> (str"Unfold " ++  pr_evaluable_reference c)
-  | Extern tac -> (str "Extern " ++ Pptactic.pr_glob_tactic tac)
-  else
   function
   | Res_pf (c,clenv) -> (str"apply " ++ prterm c)
   | ERes_pf (c,clenv) -> (str"eapply " ++ prterm c)
@@ -700,10 +683,7 @@ let trivial dbnames gl =
 	 try 
 	   searchtable_map x
 	 with Not_found -> 
-	   if !Options.v7 then
-	     error ("Trivial: "^x^": No such Hint database")
-	   else
-	     error ("trivial: "^x^": No such Hint database"))
+	   error ("trivial: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
   tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
@@ -802,10 +782,7 @@ let auto n dbnames gl =
 	 try 
 	   searchtable_map x
 	 with Not_found -> 
-	   if !Options.v7 then
-	     error ("Auto: "^x^": No such Hint database")
-	   else
-	     error ("auto: "^x^": No such Hint database"))
+	   error ("auto: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
   let hyps = pf_hyps gl in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 6cf0cc981..9eed8ecd3 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -8,8 +8,6 @@
 
 (* $Id$ *)
 
-open Ast
-open Coqast
 open Equality
 open Hipattern
 open Names
@@ -51,7 +49,8 @@ let print_rewrite_hintdb bas =
      (fun (c,typ,d,t) ->
        str (if d then "rewrite -> " else "rewrite <- ") ++
        Printer.prterm c ++ str " of type " ++ Printer.prterm typ ++
-       str " then use tactic " ++ Pptactic.pr_glob_tactic t) hints)
+       str " then use tactic " ++ 
+       Pptacticnew.pr_glob_tactic (Global.env()) t) hints)
  with
   Not_found -> 
    errorlabstrm "AutoRewrite" 
diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index 32a678410..cd8a59136 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -129,7 +129,6 @@ open Libobject
 open Library
 open Pattern
 open Matching
-open Ast
 open Pcoq
 open Tacexpr
 open Libnames
@@ -266,11 +265,10 @@ let match_dpat dp cls gls =
     | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) ->
         let hl = match lo with
             Some l -> l
-          | None -> List.map (fun id -> (id,[],(InHyp,ref None)))
-                     (pf_ids_of_hyps gls) in
+          | None -> List.map (fun id -> (id,[],InHyp)) (pf_ids_of_hyps gls) in
         if not
           (List.for_all
-            (fun (id,_,(hl,_)) ->
+            (fun (id,_,hl) ->
               let cltyp = pf_get_hyp_typ gls id in
               let cl = pf_concl gls in
               (hl=InHyp) &
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index e0cc336ca..232266e26 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -47,11 +47,8 @@ let e_resolve_with_bindings_tac  (c,lbind) gl =
 
 let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
 			     
-(* V8 TACTIC EXTEND eexact
+TACTIC EXTEND eexact
 | [ "eexact" constr(c) ] -> [ e_give_exact c ]
-END*)
-TACTIC EXTEND Eexact
-| [ "EExact" constr(c) ] -> [ e_give_exact c ]
 END
 
 let e_give_exact_constr = h_eexact
@@ -61,11 +58,8 @@ let registered_e_assumption gl =
               (pf_ids_of_hyps gl)) gl
 
 (* This automatically define h_eApply (among other things) *)
-(*V8 TACTIC EXTEND eapply
-  [ "eapply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ]
-END*)
 TACTIC EXTEND eapply
-  [ "EApply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ]
+  [ "eapply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ]
 END
 
 let vernac_e_resolve_constr c = h_eapply (c,NoBindings)
@@ -106,33 +100,30 @@ let e_right = e_constructor_tac (Some 2) 2
 let e_split = e_constructor_tac (Some 1) 1
 
 (* This automatically define h_econstructor (among other things) *)
-(*V8 TACTIC EXTEND eapply
-  [ "econstructor" integer(n) with_bindings(c) ] -> [ e_constructor_tac None n c ]
-END*)
 TACTIC EXTEND econstructor
-  [ "EConstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ]
-  | [ "EConstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ]
-  | [ "EConstructor" tactic_opt(t) ] -> [ e_any_constructor (option_app Tacinterp.eval_tactic t) ] 
+  [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ]
+| [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ]
+| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_app Tacinterp.eval_tactic t) ] 
       END
 
 TACTIC EXTEND eleft
-  [ "ELeft" "with" bindings(l) ] -> [e_left l]
-  | [ "ELeft"] -> [e_left NoBindings]
+  [ "eleft" "with" bindings(l) ] -> [e_left l]
+| [ "eleft"] -> [e_left NoBindings]
 END
 
 TACTIC EXTEND eright
-  [ "ERight" "with" bindings(l) ] -> [e_right l]
-  | [ "ERight" ] -> [e_right NoBindings]
+  [ "eright" "with" bindings(l) ] -> [e_right l]
+| [ "eright" ] -> [e_right NoBindings]
 END
 
 TACTIC EXTEND esplit
-  [ "ESplit" "with" bindings(l) ] -> [e_split l]
-  | [ "ESplit"] -> [e_split NoBindings]
+  [ "esplit" "with" bindings(l) ] -> [e_split l]
+| [ "esplit"] -> [e_split NoBindings]
 END
 
 
 TACTIC EXTEND eexists
-  [ "EExists" bindings(l) ] -> [e_split l]
+  [ "eexists" bindings(l) ] -> [e_split l]
 END
 
 
@@ -161,29 +152,10 @@ let prolog_tac l n gl =
   with UserError ("Refiner.tclFIRST",_) ->
     errorlabstrm "Prolog.prolog" (str "Prolog failed")
 
-(* V8 TACTIC EXTEND prolog
+TACTIC EXTEND prolog
 | [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
-END*)
-TACTIC EXTEND Prolog
-| [ "Prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
 END
 
-(*
-let vernac_prolog =
-  let uncom = function
-    | Constr c -> c
-    | _ -> assert false
-  in
-  let gentac = 
-    hide_tactic "Prolog"
-      (function
-	 | (Integer n) :: al -> prolog_tac (List.map uncom al) n
-	 | _ -> assert false)
-  in 
-  fun coms n -> 
-    gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms))
-*)
-
 open Auto
 
 (***************************************************************************)
@@ -433,14 +405,7 @@ ARGUMENT EXTEND hintbases
 | [ ] -> [ Some [] ]
 END
 
-TACTIC EXTEND EAuto
-| [ "EAuto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
+TACTIC EXTEND eauto
+| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
     [ gen_eauto false (make_dimension n p) db ]
 END
-
-V7 TACTIC EXTEND EAutodebug
-| [ "EAutod" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
-    [ gen_eauto true (make_dimension n p) db ]
-END
-
-
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 9d19d37e8..1ef4b928d 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -177,12 +177,12 @@ let compare c1 c2 g =
 
 (* User syntax *)
 
-TACTIC EXTEND DecideEquality
-  [ "Decide" "Equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ]
-| [ "Decide" "Equality" ] -> [ decideGralEquality ]
+TACTIC EXTEND decide_equality
+  [ "decide" "equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ]
+| [ "decide" "equality" ] -> [ decideGralEquality ]
 END
 
-TACTIC EXTEND Compare
-| [ "Compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+TACTIC EXTEND compare
+| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
 END
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 23e4d311c..04667d306 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -125,7 +125,7 @@ let rewriteRL_clause = function
 
 (* Replacing tactics *)
 
-(* eqt,sym_eqt : equality on Type and its symmetry theorem
+(* eq,sym_eq : equality on Type and its symmetry theorem
    c2 c1 : c1 is to be replaced by c2
    unsafe : If true, do not check that c1 and c2 are convertible
    gl : goal *)
@@ -134,8 +134,8 @@ let abstract_replace clause c2 c1 unsafe gl =
   let t1 = pf_type_of gl c1 
   and t2 = pf_type_of gl c2 in
   if unsafe or (pf_conv_x gl t1 t2) then
-    let e = (build_coq_eqT_data ()).eq in
-    let sym = (build_coq_eqT_data ()).sym in
+    let e = (build_coq_eq_data ()).eq in
+    let sym = (build_coq_eq_data ()).sym in
     let eq = applist (e, [t1;c1;c2]) in
     tclTHENS (assert_tac false Anonymous eq)
       [onLastHyp (fun id -> 
@@ -1030,8 +1030,7 @@ let unfold_body x gl =
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis") in
   let aft = afterHyp x gl in
-  let hl = List.fold_right
-    (fun (y,yval,_) cl -> (y,[],(InHyp,ref None)) :: cl) aft [] in
+  let hl = List.fold_right (fun (y,yval,_) cl -> (y,[],InHyp) :: cl) aft [] in
   let xvar = mkVar x in
   let rfun _ _ c = replace_term xvar xval c in
   tclTHENLIST
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index a31bc2cf0..5ff27a8e9 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -50,7 +50,8 @@ END
 
 let pr_gen prc _prlc _prtac c = prc c
 
-let pr_rawc _prc _prlc _prtac raw = Ppconstr.pr_rawconstr raw
+let pr_rawc _prc _prlc _prtac raw = 
+  Ppconstrnew.pr_constr (Constrextern.extern_rawconstr Idset.empty raw)
 
 let interp_raw _ _ (t,_) = t
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 3cc73e21d..fbd881789 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -15,127 +15,119 @@ open Pcoq
 open Genarg
 open Extraargs
 open Mod_subst
+open Names
 
 (* Equality *)
 open Equality
 
-TACTIC EXTEND Rewrite
-| [ "Rewrite" orient(b) constr_with_bindings(c) ] ->
+TACTIC EXTEND rewrite
+| [ "rewrite" orient(b) constr_with_bindings(c) ] ->
     [general_rewrite_bindings b c]
 END
 
-TACTIC EXTEND RewriteIn
-| [ "Rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] ->
+TACTIC EXTEND rewrite_in
+| [ "rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] ->
     [general_rewrite_bindings_in b h c]
 END
 
 let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
 
-TACTIC EXTEND Replace
-| [ "Replace" constr(c1) "with" constr(c2) ] ->
+TACTIC EXTEND replace
+| [ "replace" constr(c1) "with" constr(c2) ] ->
     [ replace c1 c2 ]
 END
 
-TACTIC EXTEND ReplaceIn
-| [ "Replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
+TACTIC EXTEND replace_in
+| [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
     [ replace_in h c1 c2 ]
 END
 
-TACTIC EXTEND Replacetermleft
-  [ "Replace" "->" constr(c)  ] -> [ replace_term_left c ]
+TACTIC EXTEND replace_term_left
+  [ "replace" "->" constr(c)  ] -> [ replace_term_left c ]
 END
 
-TACTIC EXTEND Replacetermright
-  [ "Replace" "<-" constr(c)  ] -> [ replace_term_right c ]
+TACTIC EXTEND replace_term_right
+  [ "replace" "<-" constr(c)  ] -> [ replace_term_right c ]
 END
 
-TACTIC EXTEND Replaceterm
-  [ "Replace" constr(c)  ] -> [ replace_term c ]
+TACTIC EXTEND replace_term
+  [ "replace" constr(c)  ] -> [ replace_term c ]
 END
 
-TACTIC EXTEND ReplacetermInleft
-  [ "Replace"  "->" constr(c) "in" hyp(h) ]
+TACTIC EXTEND replace_term_in_left
+  [ "replace"  "->" constr(c) "in" hyp(h) ]
   -> [ replace_term_in_left c h ]
 END
 
-TACTIC EXTEND ReplacetermInright
-  [ "Replace"  "<-" constr(c) "in" hyp(h) ]
+TACTIC EXTEND replace_term_in_right
+  [ "replace"  "<-" constr(c) "in" hyp(h) ]
   -> [ replace_term_in_right c h ]
 END
 
-TACTIC EXTEND ReplacetermIn
-  [ "Replace" constr(c) "in" hyp(h) ]
+TACTIC EXTEND replace_term_in
+  [ "replace" constr(c) "in" hyp(h) ]
   -> [ replace_term_in c h ]
 END
 
-TACTIC EXTEND DEq
-  [ "Simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]
+TACTIC EXTEND simplify_eq
+  [ "simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]
 END
 
-TACTIC EXTEND Discriminate
-  [ "Discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ]
+TACTIC EXTEND discriminate
+  [ "discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ]
 END
 
 let h_discrHyp id = h_discriminate (Some id)
 
-TACTIC EXTEND Injection
-  [ "Injection" quantified_hypothesis_opt(h) ] -> [ injClause h ]
+TACTIC EXTEND injection
+  [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause h ]
 END
 
 let h_injHyp id = h_injection (Some id)
 
-TACTIC EXTEND ConditionalRewrite
-| [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c) ]
+TACTIC EXTEND conditional_rewrite
+| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ]
     -> [ conditional_rewrite b (snd tac) c ]
-| [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c)
+| [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c)
     "in" hyp(h) ]
     -> [ conditional_rewrite_in b h (snd tac) c ]
 END
 
-TACTIC EXTEND DependentRewrite
-| [ "Dependent" "Rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
-| [ "Dependent" "Rewrite" orient(b) constr(c) "in" hyp(id) ]
+TACTIC EXTEND dependent_rewrite
+| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
+| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
     -> [ rewriteInHyp b c id ]
 END
 
-TACTIC EXTEND CutRewrite
-| [ "CutRewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
-| [ "CutRewrite" orient(b) constr(eqn) "in" hyp(id) ]
+TACTIC EXTEND cut_rewrite
+| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
+| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
     -> [ cutRewriteInHyp b eqn id ]
 END
 
 (* Contradiction *)
 open Contradiction
 
-TACTIC EXTEND Absurd
- [ "Absurd" constr(c) ] -> [ absurd c ]
+TACTIC EXTEND absurd
+ [ "absurd" constr(c) ] -> [ absurd c ]
 END
 
-TACTIC EXTEND Contradiction
- [ "Contradiction" constr_with_bindings_opt(c) ] -> [ contradiction c ]
+TACTIC EXTEND contradiction
+ [ "contradiction" constr_with_bindings_opt(c) ] -> [ contradiction c ]
 END
 
 (* AutoRewrite *)
 
 open Autorewrite
-TACTIC EXTEND AutorewriteV7
-  [ "AutoRewrite" "[" ne_preident_list(l) "]" ] ->
-    [ autorewrite Refiner.tclIDTAC l ]
-| [ "AutoRewrite" "[" ne_preident_list(l) "]" "using" tactic(t) ] ->
-    [ autorewrite (snd t) l ]
-| [ "AutoRewrite" "[" ne_preident_list(l) "]" "in" ident(id) ] ->
-    [ autorewrite_in id Refiner.tclIDTAC l ]
-| [ "AutoRewrite" "[" ne_preident_list(l) "]" "in" ident(id) "using" tactic(t) ] ->
-    [ autorewrite_in id (snd t) l ]
-END
-TACTIC EXTEND AutorewriteV8
-  [ "AutoRewrite" "with" ne_preident_list(l) ] ->
+
+TACTIC EXTEND autorewrite
+  [ "autorewrite" "with" ne_preident_list(l) ] ->
     [ autorewrite Refiner.tclIDTAC l ]
-| [ "AutoRewrite" "with" ne_preident_list(l) "using" tactic(t) ] ->
+| [ "autorewrite" "with" ne_preident_list(l) "using" tactic(t) ] ->
     [ autorewrite (snd t) l ]
-| [ "AutoRewrite" "with" ne_preident_list(l) "in" ident(id) ] ->
+| [ "autorewrite" "with" ne_preident_list(l) "in" ident(id) ] ->
     [ autorewrite_in id Refiner.tclIDTAC l ]
-| [ "AutoRewrite" "with" ne_preident_list(l) "in" ident(id) "using" tactic(t) ] ->
+| [ "autorewrite" "with" ne_preident_list(l) "in" ident(id) "using" tactic(t) ] ->
     [ autorewrite_in id (snd t) l ]
 END
 
@@ -144,17 +136,7 @@ let add_rewrite_hint name ort t lcsr =
   let f c = Constrintern.interp_constr sigma env c, ort, t in
   add_rew_rules name (List.map f lcsr)
 
-(* V7 *)
-VERNAC COMMAND EXTEND HintRewriteV7
-  [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) ] ->
-  [ add_rewrite_hint b o (Tacexpr.TacId "") l ]
-| [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b)
-    "using" tactic(t) ] ->
-  [ add_rewrite_hint b o t l ]
-END
-
-(* V8 *)
-VERNAC COMMAND EXTEND HintRewriteV8
+VERNAC COMMAND EXTEND HintRewrite
   [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident(b) ] ->
   [ add_rewrite_hint b o (Tacexpr.TacId "") l ]
 | [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t)
@@ -167,8 +149,8 @@ END
 
 open Refine
 
-TACTIC EXTEND Refine
-  [ "Refine" casted_open_constr(c) ] -> [ refine c ]
+TACTIC EXTEND refine
+  [ "refine" casted_open_constr(c) ] -> [ refine c ]
 END
 
 let refine_tac = h_refine
@@ -177,33 +159,33 @@ let refine_tac = h_refine
 
 open Setoid_replace
 
-TACTIC EXTEND SetoidReplace
-   [ "Setoid_replace" constr(c1) "with" constr(c2) ] ->
+TACTIC EXTEND setoid_replace
+   [ "setoid_replace" constr(c1) "with" constr(c2) ] ->
      [ setoid_replace None c1 c2 ~new_goals:[] ]
- | [ "Setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel)] ->
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel)] ->
      [ setoid_replace (Some rel) c1 c2 ~new_goals:[] ]
- | [ "Setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) ] ->
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) ] ->
      [ setoid_replace None c1 c2 ~new_goals:l ]
- | [ "Setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] ->
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] ->
      [ setoid_replace (Some rel) c1 c2 ~new_goals:l ]
- | [ "Setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) ] ->
      [ setoid_replace_in h None c1 c2 ~new_goals:[] ]
- | [ "Setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel)] ->
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel)] ->
      [ setoid_replace_in h (Some rel) c1 c2 ~new_goals:[] ]
- | [ "Setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] ->
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] ->
      [ setoid_replace_in h None c1 c2 ~new_goals:l ]
- | [ "Setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] ->
+ | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] ->
      [ setoid_replace_in h (Some rel) c1 c2 ~new_goals:l ]
 END
 
-TACTIC EXTEND SetoidRewrite
-   [ "Setoid_rewrite" orient(b) constr(c) ]
+TACTIC EXTEND setoid_rewrite
+   [ "setoid_rewrite" orient(b) constr(c) ]
    -> [ general_s_rewrite b c ~new_goals:[] ]
- | [ "Setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ]
+ | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ]
    -> [ general_s_rewrite b c ~new_goals:l ]
- | [ "Setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] ->
+ | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] ->
       [ general_s_rewrite_in h b c ~new_goals:[] ]
- | [ "Setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] ->
+ | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] ->
       [ general_s_rewrite_in h b c ~new_goals:l ]
 END
 
@@ -241,17 +223,17 @@ VERNAC COMMAND EXTEND AddRelation3
    [ add_relation n a aeq None None (Some t) ]
 END
 
-TACTIC EXTEND SetoidSymmetry
-   [ "Setoid_symmetry" ] -> [ setoid_symmetry ]
- | [ "Setoid_symmetry" "in" ident(n) ] -> [ setoid_symmetry_in n ]
+TACTIC EXTEND setoid_symmetry
+   [ "setoid_symmetry" ] -> [ setoid_symmetry ]
+ | [ "setoid_symmetry" "in" ident(n) ] -> [ setoid_symmetry_in n ]
 END
 
-TACTIC EXTEND SetoidReflexivity
-   [ "Setoid_reflexivity" ] -> [ setoid_reflexivity ]
+TACTIC EXTEND setoid_reflexivity
+   [ "setoid_reflexivity" ] -> [ setoid_reflexivity ]
 END
 
-TACTIC EXTEND SetoidTransitivity
-   [ "Setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ]
+TACTIC EXTEND setoid_transitivity
+   [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ]
 END
 
 (* Inversion lemmas (Leminv) *)
@@ -302,34 +284,27 @@ END
 
 (* Subst *)
 
-TACTIC EXTEND Subst
-| [ "Subst" ne_var_list(l) ] -> [ subst l ]
-| [ "Subst" ] -> [ subst_all ]
+TACTIC EXTEND subst
+| [ "subst" ne_var_list(l) ] -> [ subst l ]
+| [ "subst" ] -> [ subst_all ]
 END
 
 open Evar_tactics
 
 (* evar creation *)
 
-TACTIC EXTEND Evar
- [ "Evar" "(" ident(id) ":" constr(typ) ")" ] ->
-    [ let_evar (Names.Name id) typ ]
-| [ "Evar" constr(typ) ] ->
-    [ let_evar Names.Anonymous typ ]
+TACTIC EXTEND evar
+  [ "evar" "(" ident(id) ":" constr(typ) ")" ] -> [ let_evar (Name id) typ ]
+| [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
 open Tacexpr
 
 TACTIC EXTEND instantiate
-  [ "Instantiate" "(" integer(i) ":=" raw(c) ")" hloc(hl) ] ->
+  [ "instantiate" "(" integer(i) ":=" raw(c) ")" hloc(hl) ] ->
     [instantiate i c hl  ]
 END
 
-V7 TACTIC EXTEND instantiate
-  [ "Instantiate" integer(i) raw(c) hloc(hl) ] ->
-    [ instantiate i c hl  ]
-END
-
 
 (** Nijmegen "step" tactic for setoid rewriting *)
 
@@ -409,14 +384,14 @@ let add_transitivity_lemma left lem =
 
 (* Vernacular syntax *)
 
-TACTIC EXTEND Stepl
-| ["Stepl" constr(c) "by" tactic(tac) ] -> [ step true c (snd tac) ]
-| ["Stepl" constr(c) ] -> [ step true c tclIDTAC ]
+TACTIC EXTEND stepl
+| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (snd tac) ]
+| ["stepl" constr(c) ] -> [ step true c tclIDTAC ]
 END
 
-TACTIC EXTEND Stepr
-| ["Stepr" constr(c) "by" tactic(tac) ] -> [ step false c (snd tac) ]
-| ["Stepr" constr(c) ] -> [ step false c tclIDTAC ]
+TACTIC EXTEND stepr
+| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (snd tac) ]
+| ["stepr" constr(c) ] -> [ step false c tclIDTAC ]
 END
 
 VERNAC COMMAND EXTEND AddStepl
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 847d0caa7..5c375ddce 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -56,16 +56,14 @@ val h_instantiate     : int -> Rawterm.rawconstr ->
 
 (* Derived basic tactics *)
 
-val h_simple_induction   : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
+val h_simple_induction   : quantified_hypothesis -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
   constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-  -> tactic
+  intro_pattern_expr option -> tactic
 val h_new_destruct    :
   constr induction_arg -> constr with_bindings option -> 
-  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-  -> tactic
+  intro_pattern_expr option -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index b91222ae9..fd2d5c9c1 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -252,12 +252,12 @@ let rec first_match matcher = function
 
 (*** Equality *)
 
-(* Patterns "(eq ?1 ?2 ?3)", "(eqT ?1 ?2 ?3)" and "(idT ?1 ?2 ?3)" *)
+(* Patterns "(eq ?1 ?2 ?3)" and "(identity ?1 ?2 ?3)" *)
 let coq_eq_pattern_gen eq = 
   lazy (PApp(PRef (Lazy.force eq), [|mkPMeta 1;mkPMeta 2;mkPMeta 3|]))
 let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
 (*let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref*)
-let coq_idT_pattern = coq_eq_pattern_gen coq_idT_ref
+let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
 
 let match_eq eqn eq_pat =
   match matches (Lazy.force eq_pat) eqn with
@@ -268,8 +268,7 @@ let match_eq eqn eq_pat =
 
 let equalities =
   [coq_eq_pattern, build_coq_eq_data;
-(*   coq_eqT_pattern, build_coq_eqT_data;*)
-   coq_idT_pattern, build_coq_idT_data]
+   coq_identity_pattern, build_coq_identity_data]
 
 let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *)
   first_match (match_eq eqn) equalities
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 481b78683..bd5c1bf41 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -258,10 +258,12 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
 (* inv_op = Inv (derives de complete inv. lemma)
  * inv_op = InvNoThining (derives de semi inversion lemma) *)
 
-let inversion_lemma_from_goal n na id sort dep_option inv_op =
+let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op =
   let pts = get_pftreestate() in
   let gl = nth_goal_of_pftreestate n pts in
-  let t = pf_get_hyp_typ gl id in
+  let t = 
+    try pf_get_hyp_typ gl id
+    with Not_found -> Pretype_errors.error_var_not_found_loc loc id in
   let env = pf_env gl and sigma = project gl in
 (* Pourquoi ??? 
   let fv = global_vars env t in
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 6617edf2c..3e12f770e 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -1,4 +1,4 @@
-
+open Util
 open Names
 open Term
 open Rawterm
@@ -12,7 +12,7 @@ val lemInv_clause :
   quantified_hypothesis -> constr -> identifier list -> tactic
 
 val inversion_lemma_from_goal :
-  int -> identifier -> identifier -> sorts -> bool ->
+  int -> identifier -> identifier located -> sorts -> bool ->
     (identifier -> tactic) -> unit
 val add_inversion_lemma_exn :
   identifier -> constr_expr -> rawsort -> bool -> (identifier -> tactic) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e4177a69a..5f2baf8f8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -32,7 +32,6 @@ open Refiner
 open Tacmach
 open Tactic_debug
 open Topconstr
-open Ast
 open Term
 open Termops
 open Tacexpr
@@ -47,11 +46,6 @@ open Inductiveops
 open Syntax_def
 open Pretyping
 
-let strip_meta id = (* For Grammar v7 compatibility *)
-  let s = string_of_id id in
-  if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
-  else id
-
 let error_syntactic_metavariables_not_allowed loc =
   user_err_loc 
     (loc,"out_ident",
@@ -131,7 +125,7 @@ let make_hyps = List.map (fun (id,_,typ) -> (id, typ))
 let constr_of_id env id = 
   construct_reference (Environ.named_context env) id
 
-(* To embed several objects in Coqast.t *)
+(* To embed tactics *)
 let ((tactic_in : (interp_sign -> raw_tactic_expr) -> Dyn.t),
      (tactic_out : Dyn.t -> (interp_sign -> raw_tactic_expr))) =
   create "tactic"
@@ -160,7 +154,7 @@ let valueOut = function
   | ast ->
     anomalylabstrm "valueOut" (str "Not a Dynamic ast: ")
 
-(* To embed constr in Coqast.t *)
+(* To embed constr *)
 let constrIn t = CDynamic (dummy_loc,constr_in t)
 let constrOut = function
   | CDynamic (_,d) ->
@@ -170,32 +164,8 @@ let constrOut = function
       anomalylabstrm "constrOut" (str "Dynamic tag should be constr")
   | ast ->
     anomalylabstrm "constrOut" (str "Not a Dynamic ast")
-let loc = dummy_loc
-
-(* Table of interpretation functions *)
-let interp_tab =
-  (Hashtbl.create 17 : (string , interp_sign -> Coqast.t -> value) Hashtbl.t)
-
-(* Adds an interpretation function *)
-let interp_add (ast_typ,interp_fun) =
-  try
-    Hashtbl.add interp_tab ast_typ interp_fun
-  with
-      Failure _ ->
-        errorlabstrm "interp_add"
-          (str "Cannot add the interpretation function for " ++ str ast_typ ++            str " twice")
-
-(* Adds a possible existing interpretation function *)
-let overwriting_interp_add (ast_typ,interp_fun) =
-  if Hashtbl.mem interp_tab ast_typ then
-  begin
-    Hashtbl.remove interp_tab ast_typ;
-    warning ("Overwriting definition of tactic interpreter command " ^ ast_typ)
-  end;
-  Hashtbl.add interp_tab ast_typ interp_fun
 
-(* Finds the interpretation function corresponding to a given ast type *)
-let look_for_interp = Hashtbl.find interp_tab
+let loc = dummy_loc
 
 (* Globalizes the identifier *)
 
@@ -249,14 +219,12 @@ let coerce_to_inductive = function
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 let atomic_mactab = ref Idmap.empty
 let add_primitive_tactic s tac =
-  (if not !Options.v7 then
-    let id = id_of_string s in
-    atomic_mactab := Idmap.add id tac !atomic_mactab)
+  let id = id_of_string s in
+  atomic_mactab := Idmap.add id tac !atomic_mactab
 
 let _ =
-  if not !Options.v7 then
-    (let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
-    List.iter
+  let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
+  List.iter
       (fun (s,t) -> add_primitive_tactic s (TacAtom(dummy_loc,t)))
       [ "red", TacReduce(Red false,nocl);
         "hnf", TacReduce(Hnf,nocl);
@@ -275,12 +243,12 @@ let _ =
         "reflexivity", TacReflexivity;
         "symmetry", TacSymmetry nocl
       ];
-    List.iter
+  List.iter
       (fun (s,t) -> add_primitive_tactic s t)
       [ "idtac",TacId "";
         "fail", TacFail(ArgArg 0,"");
         "fresh", TacArg(TacFreshId None)
-      ])
+      ]
  
 let lookup_atomic id = Idmap.find id !atomic_mactab
 let is_atomic id = Idmap.mem id !atomic_mactab
@@ -697,18 +665,18 @@ let rec intern_atomic lf ist x =
   | TacDAuto (n,p) -> TacDAuto (option_app (intern_int_or_var ist) n,p)
 
   (* Derived basic tactics *)
-  | TacSimpleInduction (h,ids) ->
-      TacSimpleInduction (intern_quantified_hypothesis ist h,ids)
-  | TacNewInduction (c,cbo,(ids,ids')) ->
+  | TacSimpleInduction h ->
+      TacSimpleInduction (intern_quantified_hypothesis ist h)
+  | TacNewInduction (c,cbo,ids) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               (option_app (intern_intro_pattern lf ist) ids,ids'))
+               (option_app (intern_intro_pattern lf ist) ids))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
-  | TacNewDestruct (c,cbo,(ids,ids')) ->
+  | TacNewDestruct (c,cbo,ids) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-	       (option_app (intern_intro_pattern lf ist) ids,ids'))
+	       (option_app (intern_intro_pattern lf ist) ids))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -757,19 +725,13 @@ let rec intern_atomic lf ist x =
       let _ = lookup_tactic opn in
       TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
   | TacAlias (loc,s,l,(dir,body)) ->
-      let l = List.map (fun (id,a) -> (strip_meta id,intern_genarg ist a)) l in
+      let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
       try TacAlias (loc,s,l,(dir,body))
       with e -> raise (locate_error_in_file (string_of_dirpath dir) e)
 
 and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr)
 
 and intern_tactic_seq ist = function
-  (* Traducteur v7->v8 *)
-  | TacAtom (_,TacReduce (Unfold [_,Ident (_,id)],_))
-      when string_of_id id = "INZ" & !Options.translate_syntax
-        -> ist.ltacvars, (TacId "")
-  (* Fin traducteur v7->v8 *)
-
   | TacAtom (loc,t) ->
       let lf = ref ist.ltacvars in
       let t = intern_atomic lf ist t in
@@ -833,7 +795,7 @@ and intern_tacarg strict ist = function
       (* $id can occur in Grammar tactic... *)
       let id = id_of_string s in
       if find_ltacvar id ist or Options.do_translate()
-      then Reference (ArgVar (adjust_loc loc,strip_meta id))
+      then Reference (ArgVar (adjust_loc loc,id))
       else error_syntactic_metavariables_not_allowed loc
   | TacCall (loc,f,l) ->
       TacCall (loc,
@@ -881,7 +843,7 @@ and intern_genarg ist x =
   | IdentArgType ->
       let lf = ref ([],[]) in
       in_gen globwit_ident(intern_ident lf ist (out_gen rawwit_ident x))
-  | HypArgType ->
+  | VarArgType ->
       in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x))
   | RefArgType ->
       in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
@@ -892,7 +854,7 @@ and intern_genarg ist x =
   | ConstrMayEvalArgType ->
       in_gen globwit_constr_may_eval 
         (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
-  | QuantHypArgType ->
+  | QuantVarArgType ->
       in_gen globwit_quant_hyp
         (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
   | RedExprArgType ->
@@ -1092,8 +1054,8 @@ let id_of_Identifier = variable_of_value
 (* Extract a constr from a value, if any *)
 let constr_of_VConstr = constr_of_value
 
-(* Interprets an variable *)
-let interp_var ist gl (loc,id) =
+(* Interprets a bound variable (especially an existing hypothesis) *)
+let interp_hyp ist gl (loc,id) =
   (* Look first in lfun for a value coercible to a variable *)
   try 
     let v = List.assoc id ist.lfun in
@@ -1108,9 +1070,6 @@ let interp_var ist gl (loc,id) =
   else
     user_err_loc (loc,"eval_variable",pr_id id ++ str " not found")
 
-(* Interprets an existing hypothesis (i.e. a declared variable) *)
-let interp_hyp = interp_var
-
 let interp_name ist = function
   | Anonymous -> Anonymous
   | Name id -> Name (interp_ident ist id)
@@ -1637,8 +1596,8 @@ and interp_genarg ist goal x =
         (interp_intro_pattern ist (out_gen globwit_intro_pattern x))
   | IdentArgType ->
       in_gen wit_ident (interp_ident ist (out_gen globwit_ident x))
-  | HypArgType ->
-      in_gen wit_var (mkVar (interp_hyp ist goal (out_gen globwit_var x)))
+  | VarArgType ->
+      in_gen wit_var (interp_hyp ist goal (out_gen globwit_var x))
   | RefArgType ->
       in_gen wit_ref (pf_interp_reference ist goal (out_gen globwit_ref x))
   | SortArgType ->
@@ -1650,7 +1609,7 @@ and interp_genarg ist goal x =
       in_gen wit_constr (pf_interp_constr ist goal (out_gen globwit_constr x))
   | ConstrMayEvalArgType ->
       in_gen wit_constr_may_eval (interp_constr_may_eval ist goal (out_gen globwit_constr_may_eval x))
-  | QuantHypArgType ->
+  | QuantVarArgType ->
       in_gen wit_quant_hyp
         (interp_declared_or_quantified_hypothesis ist goal
           (out_gen globwit_quant_hyp x))
@@ -1770,21 +1729,18 @@ and interp_atomic ist gl = function
   | TacDAuto (n,p) -> Auto.h_dauto (option_app (interp_int_or_var ist) n,p)
 
   (* Derived basic tactics *)
-  | TacSimpleInduction (h,ids) ->
-      let h =
-        if !Options.v7 then interp_declared_or_quantified_hypothesis ist gl h
-        else interp_quantified_hypothesis ist h in
-      h_simple_induction (h,ids)
-  | TacNewInduction (c,cbo,(ids,ids')) ->
+  | TacSimpleInduction h ->
+      h_simple_induction (interp_quantified_hypothesis ist h)
+  | TacNewInduction (c,cbo,ids) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (option_app (interp_intro_pattern ist) ids,ids')
+        (option_app (interp_intro_pattern ist) ids)
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist h)
-  | TacNewDestruct (c,cbo,(ids,ids')) -> 
+  | TacNewDestruct (c,cbo,ids) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (option_app (interp_intro_pattern ist) ids,ids')
+        (option_app (interp_intro_pattern ist) ids)
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist h1 in
       let h2 = interp_quantified_hypothesis ist h2 in
@@ -1857,8 +1813,8 @@ and interp_atomic ist gl = function
 	VIntroPattern (out_gen globwit_intro_pattern x)
     | IdentArgType -> 
         VIntroPattern (IntroIdentifier (out_gen globwit_ident x))
-    | HypArgType ->
-	VConstr (mkVar (interp_var ist gl (out_gen globwit_var x)))
+    | VarArgType ->
+	VConstr (mkVar (interp_hyp ist gl (out_gen globwit_var x)))
     | RefArgType -> 
         VConstr (constr_of_global 
           (pf_interp_reference ist gl (out_gen globwit_ref x)))
@@ -1872,7 +1828,7 @@ and interp_atomic ist gl = function
     | TacticArgType n -> 
 	val_interp ist gl (out_gen (globwit_tactic n) x)
     | StringArgType | BoolArgType
-    | QuantHypArgType | RedExprArgType 
+    | QuantVarArgType | RedExprArgType 
     | OpenConstrArgType _ | ConstrWithBindingsArgType | BindingsArgType 
     | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
@@ -2155,7 +2111,7 @@ and subst_genarg subst (x:glob_generic_argument) =
   | IntroPatternArgType ->
       in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
   | IdentArgType -> in_gen globwit_ident (out_gen globwit_ident x)
-  | HypArgType -> in_gen globwit_var (out_gen globwit_var x)
+  | VarArgType -> in_gen globwit_var (out_gen globwit_var x)
   | RefArgType ->
       in_gen globwit_ref (subst_global_reference subst 
 	(out_gen globwit_ref x))
@@ -2165,7 +2121,7 @@ and subst_genarg subst (x:glob_generic_argument) =
       in_gen globwit_constr (subst_rawconstr subst (out_gen globwit_constr x))
   | ConstrMayEvalArgType ->
       in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
-  | QuantHypArgType ->
+  | QuantVarArgType ->
       in_gen globwit_quant_hyp
         (subst_declared_or_quantified_hypothesis subst 
           (out_gen globwit_quant_hyp x))
@@ -2280,11 +2236,6 @@ let glob_tactic_env l env x =
     { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env })
     x
 
-let glob_tactic_env_v7 l env x = 
-  intern_tactic
-    { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env }
-    x
-
 let interp_redexp env evc r = 
   let ist = { lfun=[]; debug=get_debug () } in
   let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = evc } in
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 8746da993..a23ce1809 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -119,8 +119,6 @@ val glob_tactic : raw_tactic_expr -> glob_tactic_expr
 
 val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
 
-val glob_tactic_env_v7 : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
-
 val eval_tactic : glob_tactic_expr -> tactic
 
 val interp : raw_tactic_expr -> tactic
@@ -131,13 +129,6 @@ val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
 
 val hide_interp : raw_tactic_expr -> tactic option -> tactic
 
-(* Adds an interpretation function *)
-val interp_add : string * (interp_sign -> Coqast.t -> value) -> unit
-
-(* Adds a possible existing interpretation function *)
-val overwriting_interp_add : string * (interp_sign -> Coqast.t -> value) ->
-                             unit
-
 (* Declare the default tactic to fill implicit arguments *)
 val declare_implicit_tactic : tactic -> unit
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 29fd46f3e..05eb17fe7 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -119,15 +119,13 @@ type clause = identifier gclause
 
 let allClauses = { onhyps=None; onconcl=true; concl_occs=[] }
 let allHyps = { onhyps=None; onconcl=false; concl_occs=[] }
-let onHyp id =
-  { onhyps=Some[(id,[],(InHyp, ref None))]; onconcl=false; concl_occs=[] }
+let onHyp id = { onhyps=Some[(id,[],InHyp)]; onconcl=false; concl_occs=[] }
 let onConcl = { onhyps=Some[]; onconcl=true; concl_occs=[] }
 
 let simple_clause_list_of cl gls =
   let hyps =
     match cl.onhyps with 
-        None ->
-          List.map (fun id -> Some(id,[],(InHyp,ref None))) (pf_ids_of_hyps gls)
+        None -> List.map (fun id -> Some(id,[],InHyp)) (pf_ids_of_hyps gls)
       | Some l -> List.map (fun h -> Some h) l in
   if cl.onconcl then None::hyps else hyps
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d1a7507c7..5e383c0c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -147,25 +147,21 @@ type tactic_reduction = env -> evar_map -> constr -> constr
 let reduct_in_concl (redfun,sty) gl = 
   convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
 
-let reduct_in_hyp redfun (id,_,(where,where')) gl =
+let reduct_in_hyp redfun (id,_,where) gl =
   let (_,c, ty) = pf_get_hyp gl id in
   let redfun' = (*under_casts*) (pf_reduce redfun gl) in
   match c with
   | None -> 
       if where = InHypValueOnly then
 	errorlabstrm "" (pr_id id ++ str "has no value");
-      if Options.do_translate () then where' := Some where;
       convert_hyp_no_check (id,None,redfun' ty) gl
   | Some b ->
-      let where =
-	if !Options.v7 & where = InHyp then InHypValueOnly else where in
       let b' = if where <> InHypTypeOnly then redfun' b else b in
       let ty' =	if where <> InHypValueOnly then redfun' ty else ty in
-      if Options.do_translate () then where' := Some where;
       convert_hyp_no_check (id,Some b',ty') gl
 
 let reduct_option redfun = function
-  | Some id -> reduct_in_hyp   (fst redfun) id 
+  | Some id -> reduct_in_hyp (fst redfun) id 
   | None    -> reduct_in_concl redfun 
 
 (* The following tactic determines whether the reduction
@@ -771,12 +767,8 @@ let check_hypotheses_occurrences_list env (_,occl) =
 
 let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
 
-(* Tactic Assert (b=false) and Pose (b=true):
-   the behaviour of Pose is corrected by the translator.
-   not that of Assert *)
-let forward b na c =
-  let wh =  if !Options.v7 && b then onConcl else nowhere in
-  letin_tac b na c wh
+(* Tactics "assert (...:=...)" (b=false) and "pose" (b=true) *)
+let forward b na c = letin_tac b na c nowhere
 
 (********************************************************************)
 (*               Exact tactics                                      *)
@@ -1127,96 +1119,49 @@ let rec first_name_buggy = function
 
 type elim_arg_kind = RecArg | IndArg | OtherArg
 
-let induct_discharge statuslists destopt avoid' ((avoid7,avoid8),ra) (names,force,rnames) gl =
-  let avoid7 = avoid7 @ avoid' in
-  let avoid8 = avoid8 @ avoid' in
+let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
+  let avoid = avoid @ avoid' in
   let (lstatus,rstatus) = statuslists in
   let tophyp = ref None in
   let rec peel_tac ra names gl = match ra with
-    | (RecArg,(recvarname7,recvarname8)) ::
-        (IndArg,(hyprecname7,hyprecname8)) :: ra' ->
+    | (RecArg,recvarname) ::
+        (IndArg,hyprecname) :: ra' ->
         let recpat,hyprec,names = match names with
           | [] ->
-              let idrec7 = (fresh_id avoid7 recvarname7 gl) in
-              let idrec8 = (fresh_id avoid8 recvarname8 gl) in
-              let idhyp7 = (fresh_id avoid7 hyprecname7 gl) in
-              let idhyp8 = (fresh_id avoid8 hyprecname8 gl) in
- 	      if Options.do_translate() &
-                (idrec7 <> idrec8 or idhyp7 <> idhyp8)
-	      then force := true;
-              let idrec = if !Options.v7 then idrec7 else idrec8 in
-              let idhyp = if !Options.v7 then idhyp7 else idhyp8 in
+              let idrec = fresh_id avoid recvarname gl in
+              let idhyp = fresh_id avoid hyprecname gl in
               (IntroIdentifier idrec, IntroIdentifier idhyp, [])
           | [IntroIdentifier id as pat] ->
-              let id7 = next_ident_away (add_prefix "IH" id) avoid7 in
-              let id8 = next_ident_away (add_prefix "IH" id) avoid8 in
- 	      if Options.do_translate() & id7 <> id8 then force := true;
-              let id = if !Options.v7 then id7 else id8 in
+              let id = next_ident_away (add_prefix "IH" id) avoid in
 	      (pat, IntroIdentifier id, [])
 	  | [pat] ->
-              let idhyp7 = (fresh_id avoid7 hyprecname7 gl) in
-              let idhyp8 = (fresh_id avoid8 hyprecname8 gl) in
- 	      if Options.do_translate() & idhyp7 <> idhyp8 then force := true;
-              let idhyp = if !Options.v7 then idhyp7 else idhyp8 in
+              let idhyp = (fresh_id avoid hyprecname gl) in
 	      (pat, IntroIdentifier idhyp, [])
           | pat1::pat2::names -> (pat1,pat2,names) in
 	(* This is buggy for intro-or-patterns with different first hypnames *)
 	if !tophyp=None then tophyp := first_name_buggy hyprec;
-	rnames := !rnames @ [recpat; hyprec];
         tclTHENLIST
 	  [ intros_pattern destopt [recpat];
 	    intros_pattern None [hyprec];
 	    peel_tac ra' names ] gl
-    | (IndArg,(hyprecname7,hyprecname8)) :: ra' ->
+    | (IndArg,hyprecname) :: ra' ->
 	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
         let pat,names = match names with
-          | [] -> IntroIdentifier (fresh_id avoid8 hyprecname8 gl), []
+          | [] -> IntroIdentifier (fresh_id avoid hyprecname gl), []
 	  | pat::names -> pat,names in
-	rnames := !rnames @ [pat];
 	tclTHEN (intros_pattern destopt [pat]) (peel_tac ra' names) gl
-    | (RecArg,(recvarname7,recvarname8)) :: ra' ->
+    | (RecArg,recvarname) :: ra' ->
         let introtac,names = match names with
           | [] -> 
-              let id8 = fresh_id avoid8 recvarname8 gl in
-	      let i =
-                if !Options.v7 then IntroAvoid avoid7 else IntroMustBe id8
-	      in
-	      (* For translator *)
-	      let id7 = fresh_id avoid7 (default_id gl
-		(match kind_of_term (pf_concl gl) with
-		  | Prod (name,t,_) -> (name,None,t)
-		  | LetIn (name,b,t,_) -> (name,Some b,t) 
-		  | _ -> raise (RefinerError IntroNeedsProduct))) gl in
-	      if Options.do_translate() & id7 <> id8 then force := true;
-              let id = if !Options.v7 then id7 else id8 in
-	      rnames := !rnames @ [IntroIdentifier id];
-	      intro_gen i destopt false, []
+              let id = fresh_id avoid recvarname gl in
+	      intro_gen (IntroMustBe id) destopt false, []
           | pat::names ->
-	      rnames := !rnames @ [pat];
 	      intros_pattern destopt [pat],names in
 	tclTHEN introtac (peel_tac ra' names) gl
     | (OtherArg,_) :: ra' ->
         let introtac,names = match names with
-          | [] -> 
-	      (* For translator *)
-	      let id7 = fresh_id avoid7 (default_id gl
-		(match kind_of_term (pf_concl gl) with
-		  | Prod (name,t,_) -> (name,None,t)
-		  | LetIn (name,b,t,_) -> (name,Some b,t) 
-		  | _ -> raise (RefinerError IntroNeedsProduct))) gl in
-	      let id8 = fresh_id avoid8 (default_id gl
-		(match kind_of_term (pf_concl gl) with
-		  | Prod (name,t,_) -> (name,None,t)
-		  | LetIn (name,b,t,_) -> (name,Some b,t) 
-		  | _ -> raise (RefinerError IntroNeedsProduct))) gl in
-	      if Options.do_translate() & id7 <> id8 then force := true;
-              let id = if !Options.v7 then id7 else id8 in
-              let avoid = if !Options.v7 then avoid7 else avoid8 in
-	      rnames := !rnames @ [IntroIdentifier id];
-	      intro_gen (IntroAvoid avoid) destopt false, []
-          | pat::names ->
-	      rnames := !rnames @ [pat];
-	      intros_pattern destopt [pat],names in
+          | [] -> intro_gen (IntroAvoid avoid) destopt false, []
+          | pat::names -> intros_pattern destopt [pat],names in
 	tclTHEN introtac (peel_tac ra' names) gl
     | [] ->
         check_unused_names names;
@@ -1400,37 +1345,6 @@ let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
       (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
   elimination_clause_scheme true elimclause indclause gl
 
-let make_up_names7 n ind (old_style,cname) = 
-  if old_style (* = V6.3 version of Induction on hypotheses *)
-  then
-    let recvarname =
-      if n=1 then 
-        cname
-      else (* To force renumbering if there is only one *)
-        make_ident (string_of_id cname ) (Some 1) in
-    recvarname, add_prefix "Hrec" recvarname, []
-  else
-    let is_hyp = atompart_of_id cname = "H" in
-    let hyprecname =
-      add_prefix "IH" (if is_hyp then Nametab.id_of_global ind else cname) in
-    let avoid =
-      if n=1 (* Only one recursive argument *)
-        or 
-        (* Rem: no recursive argument (especially if Destruct) *)
-        n=0 (* & atompart_of_id cname <> "H" (* for 7.1 compatibility *)*)
-      then []
-      else
-        (* Forbid to use cname, cname0, hyprecname and hyprecname0 *)
-        (* in order to get names such as f1, f2, ... *)
-        let avoid =
-          (make_ident (string_of_id cname) (Some 0)) ::(*here for 7.1 cmpat*)
-          (make_ident (string_of_id hyprecname) None) ::
-          (make_ident (string_of_id hyprecname) (Some 0)) :: [] in
-        if atompart_of_id cname <> "H" then
-          (make_ident (string_of_id cname) None) :: avoid
-        else avoid in
-    cname, hyprecname, avoid
-
 let make_base n id =
   if n=0 or n=1 then id
   else
@@ -1438,7 +1352,7 @@ let make_base n id =
     (* digits *)
     id_of_string (atompart_of_id (make_ident (string_of_id id) (Some 0)))
 
-let make_up_names8 n ind (_,cname) = 
+let make_up_names n ind (_,cname) = 
   let is_hyp = atompart_of_id cname = "H" in
   let base = string_of_id (make_base n cname) in
   let hyprecname =
@@ -1519,16 +1433,13 @@ let compute_elim_signature elimt names_info =
     | (_,None,t)::brs ->
 	(match try Some (check_branch p t) with Exit -> None with
 	 | Some l ->
-	     let n7 = List.fold_left
-	       (fun n b -> if b=IndArg then n+1 else n) 0 l in
-	     let n8 = List.fold_left
+	     let n = List.fold_left
 	       (fun n b -> if b=RecArg then n+1 else n) 0 l in
-             let recvarname7, hyprecname7, avoid7 = make_up_names7 n7 indt names_info in
-             let recvarname8, hyprecname8, avoid8 = make_up_names8 n8 indt names_info in
+             let recvarname, hyprecname, avoid = 
+	       make_up_names n indt names_info in
 	     let namesign = List.map
-	       (fun b -> (b,if b=IndArg then (hyprecname7,hyprecname8)
-                else (recvarname7,recvarname8))) l in
-	     ((avoid7,avoid8),namesign) :: find_branches (p+1) brs
+	       (fun b -> (b,if b=IndArg then hyprecname else recvarname)) l in
+	     (avoid,namesign) :: find_branches (p+1) brs
 	 | None -> error_ind_scheme "the branches of")
     | (_,Some _,_)::_ -> error_ind_scheme "the branches of"
     | [] ->
@@ -1559,7 +1470,7 @@ let find_elim_signature isrec style elim hyp0 gl =
   let nparams,indref,indsign = compute_elim_signature elimt name_info in
   (elimc,elimt,nparams,indref,indsign)
 
-let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl =
+let induction_from_context isrec elim_info hyp0 names gl =
   (*test suivant sans doute inutile car refait par le letin_tac*)
   if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
     errorlabstrm "induction" 
@@ -1572,11 +1483,6 @@ let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl =
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let names = compute_induction_names (Array.length indsign) names in
-  (* For translator *)
-  let names' = Array.map ref (Array.make (Array.length indsign) []) in
-  let b = ref false in
-  b_rnames := (b,Array.to_list names')::!b_rnames;
-  let names = array_map2 (fun n n' -> (n,b,n')) names names' in
   (* End translator *)
   let dephyps = List.map (fun (id,_,_) -> id) deps in
   let args =
@@ -1647,23 +1553,12 @@ let new_destruct = new_induct_destruct false
 let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim)
 let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
 
-(* This was Induction in 6.3 (hybrid form) *)
-let induction_from_context_old_style hyp b_ids gl =
-  let elim_info = find_elim_signature true true None hyp gl in
-  let x = induction_from_context true elim_info hyp (None,b_ids) gl in
-  (* For translator *) fst (List.hd !b_ids) := true;
-  x
-
-let simple_induct_id hyp b_ids =
-  if !Options.v7 then
-    tclORELSE (raw_induct hyp) (induction_from_context_old_style hyp b_ids)
-  else
-    raw_induct hyp
+let simple_induct_id hyp = raw_induct hyp
 let simple_induct_nodep = raw_induct_nodep
 
 let simple_induct = function
-  | NamedHyp id,b_ids -> simple_induct_id id b_ids
-  | AnonHyp n,_ -> simple_induct_nodep n
+  | NamedHyp id -> simple_induct_id id
+  | AnonHyp n -> simple_induct_nodep n
 
 (* Destruction tactics *)
 
@@ -1912,8 +1807,7 @@ let abstract_subproof name tac gls =
   let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
   if occur_existential concl then
-    if !Options.v7 then error "Abstract cannot handle existentials"
-    else error "\"abstract\" cannot handle existentials";
+    error "\"abstract\" cannot handle existentials";
   let lemme =
     start_proof na (IsGlobal (Proof Lemma)) secsign concl (fun _ _ -> ());
     let _,(const,kind,_) =
@@ -1955,9 +1849,7 @@ let admit_as_an_axiom gls =
   let name = add_suffix (get_current_proof_name ()) "_admitted" in
   let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
   let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
-  if occur_existential concl then
-    if !Options.v7 then error "admit cannot handle existentials"
-    else error "\"admit\" cannot handle existentials";
+  if occur_existential concl then error "\"admit\" cannot handle existentials";
   let axiom =
     let cd = Entries.ParameterEntry concl in
     let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f3da4a8c9..91c6731b7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -175,11 +175,10 @@ val general_elim_in :
 val default_elim  : constr with_bindings -> tactic
 val simplest_elim : constr -> tactic
 val elim          : constr with_bindings -> constr with_bindings option -> tactic
-val simple_induct     : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
+val simple_induct : quantified_hypothesis -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-  -> tactic
+  intro_pattern_expr option -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -188,8 +187,7 @@ val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
 val new_destruct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref
-  -> tactic
+  intro_pattern_expr option -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)
 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index e62b50bd0..3c65fe159 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -10,8 +10,6 @@
 
 (*i $Id$ i*)
 
-open Ast
-open Coqast
 open Hipattern
 open Names
 open Libnames
@@ -171,39 +169,11 @@ let tauto g =
 
 let default_intuition_tac = interp <:tactic< auto with * >>
 
-let q_elim tac=
-  <:tactic<
-  match goal with 
-    x : ?X1, H : ?X1 -> _ |- _ => generalize (H x); clear H; $tac
-  end >>
-
-let rec lfo n gl=
-  if n=0 then (tclFAIL 0 "LinearIntuition failed" gl) else
-    let p=if n<0 then n else (n-1) in
-    let lfo_rec=q_elim (Tacexpr.TacArg (valueIn (VTactic(dummy_loc,lfo p)))) in
-      intuition_gen (interp lfo_rec) gl
-
-let lfo_wrap n gl= 
-  try lfo n gl
-  with
-    Refiner.FailError _ | UserError _ ->
-      errorlabstrm "LinearIntuition" [< str "LinearIntuition failed." >]
-
-TACTIC EXTEND Tauto
-| [ "Tauto" ] -> [ tauto ]
-END
-(* Obsolete sinve V8.0
-TACTIC EXTEND TSimplif
-| [ "Simplif" ] -> [ simplif_gen ]
+TACTIC EXTEND tauto
+| [ "tauto" ] -> [ tauto ]
 END
-*)
-TACTIC EXTEND Intuition
-| [ "Intuition" ] -> [ intuition_gen default_intuition_tac ]
-| [ "Intuition" tactic(t) ] -> [ intuition_gen (snd t) ]
-END
-(* Obsolete since V8.0
-TACTIC EXTEND LinearIntuition
-| [ "LinearIntuition" ] -> [ lfo_wrap (-1)]
-| [ "LinearIntuition" integer(n)] -> [ lfo_wrap n]
+
+TACTIC EXTEND intuition
+| [ "intuition" ] -> [ intuition_gen default_intuition_tac ]
+| [ "intuition" tactic(t) ] -> [ intuition_gen (snd t) ]
 END
-*)