diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 91711c2f74..73aa4c3373 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1967,7 +1967,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in tclTHEN (tclEVARS sigma) - (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl)) + (Proofview.V82.of_tactic (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))) gl end end |