diff options
| author | herbelin | 2006-01-11 11:09:59 +0000 |
|---|---|---|
| committer | herbelin | 2006-01-11 11:09:59 +0000 |
| commit | 17d4fca7d5afa070ba0157fd5a636a858f42c873 (patch) | |
| tree | e35e5fbf3f60b50638411a6676481effe8aef4db /tactics | |
| parent | dcaefd4a668617504aaf335ed346598b03a80ba1 (diff) | |
Résidus du traducteur v7 -> v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
1 files changed, 1 insertions, 8 deletions
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, |