diff options
| -rw-r--r-- | contrib/field/field.ml4 | 2 | ||||
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 8 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 27 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1680.v (renamed from test-suite/bugs/opened/shouldnotfail/1680.v) | 0 |
5 files changed, 22 insertions, 18 deletions
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index b8a978d84e..93de6118b6 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -159,7 +159,7 @@ let field g = | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t | _ -> error "The statement is not built from Leibniz' equality" in let th = VConstr (lookup (pf_env g) typ) in - (interp_tac_gen [(id_of_string "FT",th)] (get_debug ()) + (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ()) <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g (* Verifies that all the terms have the same type and gives the right theory *) diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 0c18f47fc4..f3a82c05ed 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -2160,7 +2160,7 @@ Theorem not_exact_divide_valid : Proof. unfold valid_hyps, not_exact_divide in |- *; intros; generalize (nth_valid ep e i lp); Simplify. - rewrite (scalar_norm_add_stable t e), <-H0. + rewrite (scalar_norm_add_stable t e), <-H1. do 2 rewrite <- scalar_norm_add_stable; simpl in *; intros. absurd (interp_term e body * k1 + k2 = 0); [ now apply OMEGA4 | symmetry; auto ]. @@ -2370,9 +2370,9 @@ Theorem exact_divide_valid : Proof. unfold valid1, exact_divide in |- *; intros k1 k2 t ep e p1; Simplify; simpl; auto; subst; - rewrite <- scalar_norm_stable; simpl; intros; - [ destruct (mult_integral _ _ (sym_eq H)); intuition - | swap H; rewrite <- H1, mult_0_l; auto + rewrite <- scalar_norm_stable; simpl; intros; + [ destruct (mult_integral _ _ (sym_eq H0)); intuition + | swap H0; rewrite <- H1, mult_0_l; auto ]. Qed. diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e2a3a9796f..0ed4965f32 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -101,8 +101,10 @@ let catch_error loc tac g = (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = - { lfun : (identifier * value) list; - debug : debug_info } + { lfun : (identifier * value) list; + avoid_ids : identifier list; (* ids inherited fromm the call context + (needed to get fresh ids) *) + debug : debug_info } let check_is_value = function | VRTactic _ -> (* These are goals produced by Match *) @@ -1243,7 +1245,7 @@ let rec constr_list_aux env = function let constr_list ist env = constr_list_aux env ist.lfun -(*Extract the identifier list from lfun: join all branches (what to do else?)*) +(* Extract the identifier list from lfun: join all branches (what to do else?)*) let rec intropattern_ids = function | IntroIdentifier id -> [id] | IntroOrAndPattern ll -> @@ -1260,7 +1262,7 @@ let default_fresh_id = id_of_string "H" let interp_fresh_id ist gl l = let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in - let avoid = extract_ids ids ist.lfun in + let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in let id = if l = [] then default_fresh_id else @@ -1613,7 +1615,8 @@ and interp_ltac_reference isapplied mustbetac ist gl = function let v = List.assoc id ist.lfun in if mustbetac then coerce_to_tactic loc id v else v | ArgArg (loc,r) -> - let v = val_interp {lfun=[];debug=ist.debug} gl (lookup r) in + let ids = extract_ids [] ist.lfun in + let v = val_interp {lfun=[];avoid_ids=ids; debug=ist.debug} gl (lookup r) in if isapplied then v else locate_tactic_call loc v and interp_tacarg ist gl = function @@ -2263,18 +2266,18 @@ let make_empty_glob_sign () = gsigma = Evd.empty; genv = Global.env() } (* Initial call for interpretation *) -let interp_tac_gen lfun debug t gl = - interp_tactic { lfun=lfun; debug=debug } +let interp_tac_gen lfun avoid_ids debug t gl = + interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug } (intern_tactic { ltacvars = (List.map fst lfun, []); ltacrecvars = []; gsigma = project gl; genv = pf_env gl } t) gl -let eval_tactic t gls = interp_tactic { lfun=[]; debug=get_debug() } t gls +let eval_tactic t gls = interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug() } t gls -let interp t = interp_tac_gen [] (get_debug()) t +let interp t = interp_tac_gen [] [] (get_debug()) t let eval_ltac_constr gl t = - interp_ltac_constr { lfun=[]; debug=get_debug() } gl + interp_ltac_constr { lfun=[]; avoid_ids=[]; debug=get_debug() } gl (intern_tactic (make_empty_glob_sign ()) t ) (* Hides interpretation for pretty-print *) @@ -2674,7 +2677,7 @@ let glob_tactic_env l env x = x let interp_redexp env sigma r = - let ist = { lfun=[]; debug=get_debug () } in + let ist = { lfun=[]; avoid_ids=[]; debug=get_debug () } in let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = sigma } in interp_red_expr ist sigma env (intern_red_expr gist r) @@ -2684,7 +2687,7 @@ let interp_redexp env sigma r = let _ = Auto.set_extern_interp (fun l -> let l = List.map (fun (id,c) -> (id,VConstr c)) l in - interp_tactic {lfun=l;debug=get_debug()}) + interp_tactic {lfun=l;avoid_ids=[];debug=get_debug()}) let _ = Auto.set_extern_intern_tac (fun l -> Options.with_option strict_check diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index b4a715983d..7f497501b4 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -40,6 +40,7 @@ type value = (* Signature for interpretation: val\_interp and interpretation functions *) and interp_sign = { lfun : (identifier * value) list; + avoid_ids : identifier list; debug : debug_info } (* Transforms an id into a constr if possible *) @@ -119,7 +120,7 @@ val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr (* Interprets tactic expressions *) -val interp_tac_gen : (identifier * value) list -> +val interp_tac_gen : (identifier * value) list -> identifier list -> debug_info -> raw_tactic_expr -> tactic val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier diff --git a/test-suite/bugs/opened/shouldnotfail/1680.v b/test-suite/bugs/closed/shouldsucceed/1680.v index 524c7bab42..524c7bab42 100644 --- a/test-suite/bugs/opened/shouldnotfail/1680.v +++ b/test-suite/bugs/closed/shouldsucceed/1680.v |