diff options
| -rw-r--r-- | ltac/coretactics.ml4 | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 42 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 | ||||
| -rw-r--r-- | test-suite/success/specialize.v | 8 |
4 files changed, 40 insertions, 17 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 321d50df38..de4d589eee 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -142,7 +142,10 @@ END TACTIC EXTEND specialize [ "specialize" constr_with_bindings(c) ] -> [ - Tacticals.New.tclDELAYEDWITHHOLES false c Tactics.specialize + Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) + ] +| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ + Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) ] END diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 23aadf3933..d4158d7872 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2859,7 +2859,7 @@ let quantify lconstr = (* Modifying/Adding an hypothesis *) -let specialize (c,lbind) = +let specialize (c,lbind) ipat = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in @@ -2880,24 +2880,36 @@ let specialize (c,lbind) = let term = applist(thd,List.map (nf_evar clause.evd) tstack) in if occur_meta term then errorlabstrm "" (str "Cannot infer an instance for " ++ + pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ str "."); clause.evd, term in let typ = Retyping.get_type_of env sigma term in - match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with - | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS sigma) - (Tacticals.New.tclTHENFIRST - (assert_before_replacing id typ) - (exact_no_check term)) - | _ -> - (* To deprecate in favor of generalize? *) - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS sigma) - (Tacticals.New.tclTHENLAST - (cut typ) - (exact_no_check term)) + let tac = + match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with + | Var id when Id.List.mem id (Tacmach.New.pf_ids_of_hyps gl) -> + (* Like assert (id:=id args) but with the concept of specialization *) + let naming,tac = + prepare_intros false (IntroIdentifier id) MoveLast ipat in + let repl = do_replace (Some id) naming in + Tacticals.New.tclTHENFIRST + (assert_before_then_gen repl naming typ tac) + (exact_no_check term) + | _ -> + match ipat with + | None -> + (* Like generalize with extra support for "with" bindings *) + (* even though the "with" bindings forces full application *) + Tacticals.New.tclTHENLAST (cut typ) (exact_no_check term) + | Some (loc,ipat) -> + (* Like pose proof with extra support for "with" bindings *) + (* even though the "with" bindings forces full application *) + let naming,tac = prepare_intros_loc loc false IntroAnonymous MoveLast ipat in + Tacticals.New.tclTHENFIRST + (assert_before_then_gen false naming typ tac) + (exact_no_check term) + in + Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) tac end } (*****************************) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 012c75091a..fb033363e8 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -174,7 +174,7 @@ val unfold_body : Id.t -> unit Proofview.tactic val keep : Id.t list -> unit Proofview.tactic val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic -val specialize : constr with_bindings -> unit Proofview.tactic +val specialize : constr with_bindings -> intro_pattern option -> unit Proofview.tactic val move_hyp : Id.t -> Id.t move_location -> unit Proofview.tactic val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 3faa1ca43a..fba05cd902 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -64,3 +64,11 @@ assert (H:=H I). match goal with H:_ |- _ => clear H end. match goal with H:_ |- _ => exact H end. Qed. + +(* Test specialize as *) + +Goal (forall x, x=0) -> 1=0. +intros. +specialize (H 1) as ->. +reflexivity. +Qed. |