From 17d4fca7d5afa070ba0157fd5a636a858f42c873 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Jan 2006 11:09:59 +0000
Subject: Résidus du traducteur v7 -> v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8d4d37f426..6c7be7d288 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,
-- 
cgit v1.2.3