diff options
| -rw-r--r-- | tactics/class_tactics.ml4 | 18 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 25 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 15 |
3 files changed, 39 insertions, 19 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index e803e8dcbc..22e95ef5d8 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -1734,14 +1734,20 @@ let relation_of_constr env c = let setoid_proof gl ty fn fallback = let env = pf_env gl in - let rel, args = relation_of_constr env (pf_concl gl) in - let evm, car = project gl, pf_type_of gl args.(0) in - try fn env evm car rel gl - with Not_found -> + try + let rel, args = relation_of_constr env (pf_concl gl) in + let evm, car = project gl, pf_type_of gl args.(0) in + fn env evm car rel gl + with e -> match fallback gl with | Some tac -> tac gl - | None -> not_declared env ty rel gl - + | None -> + match e with + | Not_found -> + let rel, args = relation_of_constr env (pf_concl gl) in + not_declared env ty rel gl + | _ -> raise e + let setoid_reflexivity gl = setoid_proof gl "reflexive" (fun env evm car rel -> apply (get_reflexive_proof env evm car rel)) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 3e0e8ca2be..11f710997e 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -189,33 +189,32 @@ Ltac simplify_eqs := (** A tactic that tries to remove trivial equality guards in induction hypotheses coming from [dependent induction]/[generalize_eqs] invocations. *) - Ltac simpl_IH_eq H := match type of H with | @JMeq _ ?x _ _ -> _ => - specialize (H (JMeq_refl x)) + refine_hyp (H (JMeq_refl x)) | _ -> @JMeq _ ?x _ _ -> _ => - specialize (H _ (JMeq_refl x)) + refine_hyp (H _ (JMeq_refl x)) | _ -> _ -> @JMeq _ ?x _ _ -> _ => - specialize (H _ _ (JMeq_refl x)) + refine_hyp (H _ _ (JMeq_refl x)) | _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => - specialize (H _ _ _ (JMeq_refl x)) + refine_hyp (H _ _ _ (JMeq_refl x)) | _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => - specialize (H _ _ _ _ (JMeq_refl x)) + refine_hyp (H _ _ _ _ (JMeq_refl x)) | _ -> _ -> _ -> _ -> _ -> @JMeq _ ?x _ _ -> _ => - specialize (H _ _ _ _ _ (JMeq_refl x)) + refine_hyp (H _ _ _ _ _ (JMeq_refl x)) | ?x = _ -> _ => - specialize (H (refl_equal x)) + refine_hyp (H (refl_equal x)) | _ -> ?x = _ -> _ => - specialize (H _ (refl_equal x)) + refine_hyp (H _ (refl_equal x)) | _ -> _ -> ?x = _ -> _ => - specialize (H _ _ (refl_equal x)) + refine_hyp (H _ _ (refl_equal x)) | _ -> _ -> _ -> ?x = _ -> _ => - specialize (H _ _ _ (refl_equal x)) + refine_hyp (H _ _ _ (refl_equal x)) | _ -> _ -> _ -> _ -> ?x = _ -> _ => - specialize (H _ _ _ _ (refl_equal x)) + refine_hyp (H _ _ _ _ (refl_equal x)) | _ -> _ -> _ -> _ -> _ -> ?x = _ -> _ => - specialize (H _ _ _ _ _ (refl_equal x)) + refine_hyp (H _ _ _ _ _ (refl_equal x)) end. Ltac simpl_IH_eqs H := repeat simpl_IH_eq H. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 9cb7725c0f..5c904e2194 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -233,6 +233,21 @@ Ltac replace_hyp H c := let H' := fresh "H" in assert(H' := c) ; clear H ; rename H' into H. +(** A tactic to refine an hypothesis by supplying some of its arguments. *) + +Ltac refine_hyp c := + let tac H := replace_hyp H c in + match c with + | ?H _ => tac H + | ?H _ _ => tac H + | ?H _ _ _ => tac H + | ?H _ _ _ _ => tac H + | ?H _ _ _ _ _ => tac H + | ?H _ _ _ _ _ _ => tac H + | ?H _ _ _ _ _ _ _ => tac H + | ?H _ _ _ _ _ _ _ _ => tac H + end. + (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto] is not enough, better rebind using [Obligation Tactic := tac] in this case, possibly using [program_simplify] to use standard goal-cleaning tactics. *) |