diff options
| author | Pierre-Marie Pédrot | 2016-05-17 22:37:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-17 22:38:40 +0200 |
| commit | f7fb1918619fcef384d4aa84938246de67c707fa (patch) | |
| tree | 6f8b1b8ba71681b06b4a74ddeee76d02a3ef09dd /tactics/autorewrite.ml | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
| parent | dadd4003b6607ccc103658f842b5efbd6d8ab57f (diff) | |
Putting all the tactics exported by the Tactics module in the new monad API.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 6d6e51536c..9ae0ab90b2 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -151,7 +151,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = begin let gl'' = if !to_be_cleared then - tclTHEN (fun _ -> gl') (tclTRY (clear [!id])) gl + tclTHEN (fun _ -> gl') (tclTRY (Proofview.V82.of_tactic (clear [!id]))) gl else gl' in id := lastid ; to_be_cleared := true ; |