diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/coretactics.ml4 | 4 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 4e2dfafb52..98b77ab357 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -231,8 +231,8 @@ END (* Fix *) TACTIC EXTEND fix - [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ] -| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ] + [ "fix" natural(n) ] -> [ Tactics.fix None n ] +| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ] END (* Cofix *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index d650cb5c6f..5e0153fcee 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1714,7 +1714,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in - let tac = Proofview.V82.tactic (Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0) in + let tac = Tactics.mutual_fix (interp_ident ist env sigma id) n l_interp 0 in Sigma.Unsafe.of_pair (tac, sigma) end } end |