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 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7838 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/constrextern.ml | 14 +++----------- interp/topconstr.ml | 2 +- tactics/tacinterp.ml | 9 +-------- 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, -- cgit v1.2.3