From 9fea58122001535bdee63317b56f2afb727167c7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 27 Feb 2015 14:05:16 +0100 Subject: Somehow fixing bug #3467. The notations using tactics in term seem now not to respect globalized names. It is not obvious that this is the expected behaviour, but at least it does not die with an anomaly. --- tactics/tacsubst.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 42e61cb57e..afffaffbe9 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -27,9 +27,8 @@ let subst_quantified_hypothesis _ x = x let subst_declared_or_quantified_hypothesis _ x = x -let subst_glob_constr_and_expr subst (c,e) = - assert (Option.is_empty e); (* e<>None only for toplevel tactics *) - (Detyping.subst_glob_constr subst c,None) +let subst_glob_constr_and_expr subst (c, e) = + (Detyping.subst_glob_constr subst c, e) let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) -- cgit v1.2.3 From 5f8c0bfbb04de58a527d373c3994592e5853d4e2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 27 Feb 2015 16:32:38 +0100 Subject: Hack so that refine_no_check accepts an argument which is a match on an inductive type with let-in in the arity (until logic.ml disappears). --- tactics/tactics.ml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ccf4795d68..ad6684e25b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1122,11 +1122,18 @@ let enforce_prop_bound_names rename tac = | _ -> tac +let rec contract_letin_in_lam_header c = + match kind_of_term c with + | Lambda (x,t,c) -> mkLambda (x,t,contract_letin_in_lam_header c) + | LetIn (x,b,t,c) -> contract_letin_in_lam_header (subst1 b c) + | _ -> c + let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in + let elim = contract_letin_in_lam_header elim in let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = (match kind_of_term (nth_arg i elimclause.templval.rebus) with @@ -1280,6 +1287,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in + let elim = contract_letin_in_lam_header elim in let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = destMeta (nth_arg i elimclause.templval.rebus) in let hypmv = @@ -3656,6 +3664,7 @@ let induction_tac with_evars params indvars elim gl = let ({elimindex=i;elimbody=(elimc,lbindelimc);elimrename=rename},elimt) = elim in let i = match i with None -> index_of_ind_arg elimt | Some i -> i in (* elimclause contains this: (elimc ?i ?j ?k...?l) *) + let elimc = contract_letin_in_lam_header elimc in let elimc = mkCast (elimc, DEFAULTcast, elimt) in let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in -- cgit v1.2.3 From fc1b3ef9d7270938cd83c524aae0383093b7a4b5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 27 Feb 2015 20:42:44 +0100 Subject: Removing the unused field ltacrecvars of tactic internalization. --- tactics/tacintern.ml | 12 +++--------- tactics/tacintern.mli | 1 - tactics/tacinterp.ml | 6 ++---- 3 files changed, 5 insertions(+), 14 deletions(-) (limited to 'tactics') diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c8b9a2084c..5cc4c835bc 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -48,12 +48,10 @@ let error_tactic_expected loc = type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; (* ltac variables and the subset of vars introduced by Intro/Let/... *) - ltacrecvars : ltac_constant Id.Map.t; - (* ltac recursive names *) genv : Environ.env } let fully_empty_glob_sign = - { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; genv = Environ.empty_env } + { ltacvars = Id.Set.empty; genv = Environ.empty_env } let make_empty_glob_sign () = { fully_empty_glob_sign with genv = Global.env () } @@ -64,8 +62,6 @@ let find_ident id ist = Id.Set.mem id ist.ltacvars || Id.List.mem id (ids_of_named_context (Environ.named_context ist.genv)) -let find_recvar qid ist = Id.Map.find qid ist.ltacrecvars - (* a "var" is a ltac var or a var introduced by an intro tactic *) let find_var id ist = Id.Set.mem id ist.ltacvars @@ -116,9 +112,7 @@ let intern_ltac_variable ist = function if find_var id ist then (* A local variable of any type *) ArgVar (loc,id) - else - (* A recursive variable *) - ArgArg (loc,find_recvar id ist) + else raise Not_found | _ -> raise Not_found @@ -801,7 +795,7 @@ let glob_tactic_env l env x = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in Flags.with_option strict_check (intern_pure_tactic - { ltacvars; ltacrecvars = Id.Map.empty; genv = env }) + { ltacvars; genv = env }) x let split_ltac_fun = function diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 2e662e5823..a6e28d568d 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -19,7 +19,6 @@ open Nametab type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; - ltacrecvars : ltac_constant Id.Map.t; genv : Environ.env } val fully_empty_glob_sign : glob_sign diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index af541b8b9e..8826875a38 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2251,8 +2251,7 @@ let interp_tac_gen lfun avoid_ids debug t = let ltacvars = Id.Map.domain lfun in interp_tactic ist (intern_pure_tactic { - ltacvars; ltacrecvars = Id.Map.empty; - genv = env } t) + ltacvars; genv = env } t) end let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t @@ -2262,8 +2261,7 @@ let _ = Proof_global.set_interp_tac interp (* [global] means that [t] should be internalized outside of goals. *) let hide_interp global t ot = let hide_interp env = - let ist = { ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty; - genv = env } in + let ist = { ltacvars = Id.Set.empty; genv = env } in let te = intern_pure_tactic ist t in let t = eval_tactic te in match ot with -- cgit v1.2.3