diff options
| author | Hugo Herbelin | 2020-08-22 15:05:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-22 15:05:48 +0200 |
| commit | 692b2de5009ba49bca72b19091ea6294b813777b (patch) | |
| tree | dc40bcb05d1e512184cf11827b2989fe2c5b69e8 /tactics | |
| parent | f149d617b631d6fc64937d3882ed3db16fdf6c8f (diff) | |
| parent | a2b4233a379951f9c07d145023201fb536098570 (diff) | |
Merge PR #12866: Less fragile scheme equality
Ack-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 14 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 13 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb2e607012..70cea89ccb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1044,12 +1044,15 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = end end -let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ()) +let drop_intro_name (_ : Id.t) = Proofview.tclUNIT () + +let intro_gen n m f d = intro_then_gen n m f d drop_intro_name let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast true false -let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false +let intro_using_then id = intro_then_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false +let intro_using id = intro_using_then id drop_intro_name let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false -let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false +let intro = intro_then drop_intro_name let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false @@ -1065,6 +1068,11 @@ let rec intros_using = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l) +let rec intros_using_then_helper tac acc = function + | [] -> tac (List.rev acc) + | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l) +let intros_using_then l tac = intros_using_then_helper tac [] l + let intros = Tacticals.New.tclREPEAT intro let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 5b397b15d0..00739306a7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -65,9 +65,11 @@ val intro_avoiding : Id.Set.t -> unit Proofview.tactic val intro_replacing : Id.t -> unit Proofview.tactic val intro_using : Id.t -> unit Proofview.tactic +val intro_using_then : Id.t -> (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intro_mustbe_force : Id.t -> unit Proofview.tactic val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic val intros_using : Id.t list -> unit Proofview.tactic +val intros_using_then : Id.t list -> (Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros_possibly_replacing : Id.t list -> unit Proofview.tactic |