diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bcb6041eff..f815830ca2 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -510,6 +510,8 @@ module New = struct (* Try the first thats solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) + let tclPROGRESS t = + Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) let tclWITHHOLES accept_unresolved_holes tac sigma x = tclEVARMAP >= fun sigma_initial -> |