diff options
| author | Gaëtan Gilbert | 2020-08-24 13:34:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-25 16:15:18 +0200 |
| commit | 495466d20d53ca33adc69a4d9f6cceb8f30d8aad (patch) | |
| tree | 31c4c0b49defed84125a0bffa4a138b4f824c231 /tactics/tactics.ml | |
| parent | a9a0307e2695e97143a8fc36ccdbfdd7de0c3820 (diff) | |
Deprecate intro_using
This is a footgun as it can refresh the name. Callers can still ignore
the generated name by doing `intro_using_then id (fun _ -> tclUNIT())`.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 70cea89ccb..eb7b7e363f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1068,6 +1068,10 @@ let rec intros_using = function | [] -> Proofview.tclUNIT() | str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l) +let rec intros_mustbe_force = function + | [] -> Proofview.tclUNIT() + | str::l -> Tacticals.New.tclTHEN (intro_mustbe_force str) (intros_mustbe_force 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) |