diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/inv.ml | 12 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.mli | 1 |
3 files changed, 12 insertions, 7 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 2efaa96b6d..081b62b18c 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -330,7 +330,7 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id If it can discriminate then the goal is proved, if not tries to use it as a rewrite rule. It erases the clause which is given as input *) -let projectAndApply as_mode thin id eqname names depids = +let projectAndApply as_mode thin avoid id eqname names depids = let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id))) (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC)) @@ -352,7 +352,7 @@ let projectAndApply as_mode thin id eqname names depids = [if as_mode then clear [id] else tclIDTAC; (tclMAP_i (false,false) neqns (function (idopt,_) -> tclTRY (tclTHEN - (intro_move idopt MoveLast) + (intro_move_avoid idopt avoid MoveLast) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id)))))) @@ -382,6 +382,7 @@ let rewrite_equations as_mode othin neqns names ba = Proofview.Goal.nf_enter begin fun gl -> let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in let first_eq = ref MoveLast in + let avoid = if as_mode then List.map pi1 nodepids else [] in match othin with | Some thin -> tclTHENLIST @@ -392,12 +393,13 @@ let rewrite_equations as_mode othin neqns names ba = (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx))); tclMAP_i (true,false) neqns (fun (idopt,names) -> (tclTHEN - (intro_move idopt MoveLast) + (intro_move_avoid idopt avoid MoveLast) (onLastHypId (fun id -> - tclTRY (projectAndApply as_mode thin id first_eq names depids))))) + tclTRY (projectAndApply as_mode thin avoid id first_eq names depids))))) names; tclMAP (fun (id,_,_) -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *) - intro_move None (if thin then MoveLast else !first_eq)) + let idopt = if as_mode then Some id else None in + intro_move idopt (if thin then MoveLast else !first_eq)) nodepids; (tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids)] | None -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c5486ce533..ca1e25fbe8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -604,10 +604,12 @@ let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false -let intro_move idopt hto = match idopt with - | None -> intro_gen (NamingAvoid []) hto true false +let intro_move_avoid idopt avoid hto = match idopt with + | None -> intro_gen (NamingAvoid avoid) hto true false | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false +let intro_move idopt hto = intro_move_avoid idopt [] hto + (**** Multiple introduction tactics ****) let rec intros_using = function diff --git a/tactics/tactics.mli b/tactics/tactics.mli index a9434d6ae7..d6e648b9b5 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -57,6 +57,7 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list val intro : unit Proofview.tactic val introf : unit Proofview.tactic val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic +val intro_move_avoid : Id.t option -> Id.t list -> Id.t move_location -> unit Proofview.tactic (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) |