Résidus du traducteur v7 -> v8

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

3 files changed, 5 insertions, 20 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3707c0f9a..40d046574 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -373,7 +373,7 @@ let bind_env sigma var v =
 let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with
   | r1, AVar id2 when List.mem id2 metas -> bind_env sigma id2 r1
   | PatVar (_,Anonymous), AHole _ -> sigma
-  | a, AHole _ when not(Options.do_translate()) -> sigma
+  | a, AHole _ -> sigma
   | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ ->
       let nparams =
 	(fst (Global.lookup_inductive ind)).Declarations.mind_nparams in
@@ -547,9 +547,7 @@ let rec extern_args extern scopes env args subscopes =
 
 let rec remove_coercions inctx = function
   | RApp (loc,RRef (_,r),args) as c
-      when
-        inctx &
-        not (!Options.raw_print or !print_coercions or Options.do_translate ())
+      when inctx & not (!Options.raw_print or !print_coercions)
       ->
       (try match Classops.hide_coercion r with
 	  | Some n when n < List.length args ->
@@ -717,13 +715,7 @@ let rec extern inctx scopes vars r =
 	 | RFix (nv,n) ->
 	     let listdecl = 
 	       Array.mapi (fun i fi ->
-                 let (bl,ty,def) =
-                   if Options.do_translate() then
-                     let n = List.fold_left
-                       (fun n (_,obd,_) -> if obd=None then n-1 else n)
-                       nv.(i) blv.(i) in
-                     share_fix_binders n (List.rev blv.(i)) tyv.(i) bv.(i)
-                   else blv.(i), tyv.(i), bv.(i) in
+                 let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
                  let (ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (name_fold Idset.add) ids vars in
                  let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index da67c9f3f..2f2a381c0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -432,7 +432,7 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
       match_ alp metas (match_ alp metas sigma c1 c2) t1 t2
   | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
   | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
-  | a, AHole _ when not(Options.do_translate()) -> sigma
+  | a, AHole _ -> sigma
   | RHole _, AHole _ -> sigma
   | (RDynamic _ | RRec _ | REvar _), _ 
   | _,_ -> raise No_match
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8d4d37f42..6c7be7d28 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -435,12 +435,6 @@ let intern_constr_gen isarity {ltacvars=lfun; gsigma=sigma; genv=env} c =
   let c' = 
     warn (Constrintern.intern_gen isarity ~ltacvars:(fst lfun,[]) sigma env) c
   in
-  begin if Options.do_translate () then try
-      (* Try to infer old case and type annotations *)
-      let _ = understand_tcc sigma env c' in 
-      (* msgerrnl (str "Typage tactique OK");*)
-      ()
-    with e -> (*msgerrnl (str "Warning: can't type tactic");*) () end;
   (c',if !strict_check then None else Some c)
 
 let intern_constr = intern_constr_gen false
@@ -794,8 +788,7 @@ and intern_tacarg strict ist = function
   | MetaIdArg (loc,s) ->
       (* $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,id))
+      if find_ltacvar id ist then Reference (ArgVar (adjust_loc loc,id))
       else error_syntactic_metavariables_not_allowed loc
   | TacCall (loc,f,l) ->
       TacCall (loc,