diff options
-rw-r--r-- | doc/refman/RefMan-tac.tex | 23 | ||||
-rw-r--r-- | tactics/eauto.ml | 3 | ||||
-rw-r--r-- | tactics/equality.ml | 8 | ||||
-rw-r--r-- | test-suite/bugs/closed/4762.v | 24 | ||||
-rw-r--r-- | test-suite/output/subst.out | 208 | ||||
-rw-r--r-- | test-suite/output/subst.v | 11 |
6 files changed, 262 insertions, 15 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index c5fd40bf1..d23a49bc6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4356,22 +4356,23 @@ vernacular command and printed using {\nobreak {\tt Print Firstorder Tries to solve the goal with {\tac} when no logical rule may apply. - \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ } - \tacindex{firstorder with} - - Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search - environment. - \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ } \tacindex{firstorder using} - Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$ - to the proof-search environment. If {\qualid}$_i$ refers to an inductive - type, it is the collection of its constructors which is added as hints. + Adds lemmas {\qualid}$_1$ \dots\ {\qualid}$_n$ to the proof-search + environment. If {\qualid}$_i$ refers to an inductive type, it is + the collection of its constructors which are added to the + proof-search environment. -\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$} + \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ } + \tacindex{firstorder with} - This combines the effects of the {\tt using} and {\tt with} options. + Adds lemmas from {\tt auto} hint bases \ident$_1$ \dots\ \ident$_n$ + to the proof-search environment. + +\item \texttt{firstorder {\tac} using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$} + + This combines the effects of the different variants of \texttt{firstorder}. \end{Variants} diff --git a/tactics/eauto.ml b/tactics/eauto.ml index ba9a2d95c..90f80a737 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -282,7 +282,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) -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 3e5b7b65f..26e4f01f2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1761,20 +1761,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 decl = + let select_equation_name decl = try let lbeq,u,(_,x,y) = find_eq_data_decompose (get_type decl) 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 (get_id decl) + | _, Var z when not (is_evaluable env (EvalVarRef z)) -> Some (get_id decl) | _ -> 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 *) diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v new file mode 100644 index 000000000..7a87b07a8 --- /dev/null +++ b/test-suite/bugs/closed/4762.v @@ -0,0 +1,24 @@ +Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q. + +Lemma foo P Q R : R = myand P Q -> P -> Q -> R. +Proof. intros ->; constructor; auto. Qed. + +Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test1. +Qed. + +Hint Extern 0 => + match goal with + | |- myand _ _ => eapply foo; [reflexivity| |] + end : test2. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test2. (* works *) +Qed. + diff --git a/test-suite/output/subst.out b/test-suite/output/subst.out index 209b2bc26..dbb9e09a4 100644 --- a/test-suite/output/subst.out +++ b/test-suite/output/subst.out @@ -26,6 +26,19 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + x, y : nat Hx : x = 0 Hy : y = 0 @@ -39,6 +52,45 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : 0 = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + H1 : 0 = 1 HA : True H2 : 0 = 2 @@ -52,6 +104,58 @@ y, z : nat Hy : y = 0 Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + H3 : 0 = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + H1 : 0 = 1 + HA : True + H2 : 0 = 2 + H3 : y = 3 + HB : True + H4 : z = 4 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 HA : True H3 : y = 3 HB : True @@ -75,6 +179,19 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + x, y : nat Hx : x = 0 Hy : y = 0 @@ -88,6 +205,45 @@ True 1 subgoal + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + HB : True + H4 : z = 4 + H3 : 0 = 3 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + HA, HB : True H4 : 0 = 4 H3 : 0 = 3 @@ -95,3 +251,55 @@ H2 : 0 = 2 ============================ True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True +1 subgoal + + x, z : nat + Hx : x = 0 + Hz : z = 0 + H1 : x = 1 + HA : True + H2 : x = 2 + HB : True + H4 : z = 4 + H3 : 0 = 3 + ============================ + True +1 subgoal + + y, z : nat + Hy : y = 0 + Hz : z = 0 + HA : True + H3 : y = 3 + HB : True + H4 : z = 4 + H1 : 0 = 1 + H2 : 0 = 2 + ============================ + True diff --git a/test-suite/output/subst.v b/test-suite/output/subst.v index e48aa6bb2..91bdd03e0 100644 --- a/test-suite/output/subst.v +++ b/test-suite/output/subst.v @@ -45,4 +45,15 @@ Show. trivial. Qed. +(* A bug revealed by OCaml 4.03 warnings *) +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +subst. +Fail clear H. (* Was working *) +Abort. +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +subst. +Fail clear H. (* Was failing before fix *) +Abort. |