From 4e3d4646788c96f16193df14a81aa79938812194 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 29 Sep 2016 09:35:07 +0200 Subject: Fix a bug in subst releaved by an OCaml warning. --- tactics/equality.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index 06a9b317a2..b4c027382a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1730,20 +1730,22 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in - let test (hyp,_,c) = + let select_equation_name (hyp,_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match kind_of_term x, kind_of_term y with - | Var z, _ | _, Var z when not (is_evaluable env (EvalVarRef z)) -> + | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> + Some hyp + | _, Var z when not (is_evaluable env (EvalVarRef z)) -> Some hyp | _ -> None with Constr_matching.PatternMatchingFailure -> None in let hyps = Proofview.Goal.hyps gl in - List.rev (List.map_filter test hyps) + List.rev (List.map_filter select_equation_name hyps) in (* Second step: treat equations *) -- cgit v1.2.3 From 844b076bf5150a107d31cd4648955c3a6538a34b Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Wed, 28 Sep 2016 10:40:54 +0200 Subject: Fix #4762. --- tactics/eauto.ml4 | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index cb206a7dd1..7e37722e93 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -291,7 +291,8 @@ module SearchProblem = struct in let rec_tacs = let l = - filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) + let concl = Reductionops.nf_evar (project g)(pf_concl g) in + filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl) in List.map (fun (lgls, cost, pp) -> -- cgit v1.2.3 From 024cf5ae087024399cc894b121437d72cd11b480 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 30 Sep 2016 16:42:54 +0200 Subject: Fix bug #4471: [generalize dependent] permits ill-typed terms in trunk. This bug was introduced by 37ab45726, because the new apply_type function was not checking that the new goal was indeed well-typed. We add this check locally in the generalize dependent tactic. --- tactics/tactics.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2d901c2dbc..2fe8e0bc34 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2807,6 +2807,8 @@ let old_generalize_dep ?(with_let=false) c gl = in let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) (cl',project gl) in + (** Check that the generalization is indeed well-typed *) + let (evd, _) = Typing.type_of env evd cl'' in let args = Context.Named.to_instance to_quantify_rev in tclTHENLIST [tclEVARS evd; -- cgit v1.2.3 From 064de6f6839c4ef963b83018812c5d4113eb2bb9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 30 Sep 2016 17:25:58 +0200 Subject: Fix bug #5045: [generalize] creates ill-typed terms in 8.6. --- tactics/tactics.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2fe8e0bc34..c550df1019 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2821,10 +2821,12 @@ let generalize_dep ?(with_let = false) c = (** *) let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let env = Proofview.Goal.env gl in let newcl, evd = List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in + let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in let tac = apply_type newcl (List.map_filter map lconstr) in Sigma.Unsafe.of_pair (tac, evd) -- cgit v1.2.3 From 89ec88f1e750cfb786de1929ef44fac70c9a29ab Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 30 Sep 2016 18:45:06 +0200 Subject: Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime. --- tactics/equality.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/equality.ml b/tactics/equality.ml index b4c027382a..95b3e2b779 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1752,15 +1752,16 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let process hyp = Proofview.Goal.enter begin fun gl -> let gl = Proofview.Goal.assume gl in + let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in let (_,_,c) = pf_get_hyp hyp gl in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else match kind_of_term x, kind_of_term y with - | Var x', _ when not (occur_term x y) -> + | Var x', _ when not (occur_term x y) && not (is_evaluable env (EvalVarRef x')) -> subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (occur_term y x) -> + | _, Var y' when not (occur_term y x) && not (is_evaluable env (EvalVarRef y')) -> subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () -- cgit v1.2.3 From cc407dc4272928944af06ee141d71ff3c9622347 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sat, 1 Oct 2016 08:37:59 +0200 Subject: Micro refactoring: use exact_no_check. This does not affect the semantics of these functions. --- tactics/tactics.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c550df1019..c8cdae53be 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1937,9 +1937,7 @@ let exact_check c = let cast_no_check cast c = Proofview.Goal.enter { enter = begin fun gl -> let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - Refine.refine ~unsafe:true { run = begin fun sigma -> - Sigma.here (Term.mkCast (c, cast, concl)) sigma - end } + exact_no_check (Term.mkCast (c, cast, concl)) end } let vm_cast_no_check c = cast_no_check Term.VMcast c @@ -1976,7 +1974,7 @@ let assumption = in if is_same_type then (Proofview.Unsafe.tclEVARS sigma) <*> - Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h } + exact_no_check (mkVar (get_id decl)) else arec gl only_eq rest in let assumption_tac = { enter = begin fun gl -> -- cgit v1.2.3