diff options
| author | Pierre-Marie Pédrot | 2016-05-16 18:34:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 21:17:25 +0200 |
| commit | 12f4c8ed277fa8368cab2e99f173339a64bcef3d (patch) | |
| tree | e6a5072d1f747d0266fe7d6af9ef666b39f3dcce /ltac | |
| parent | dc8750d166cffd846619d2de20e02a4e31c6357f (diff) | |
Put the "fix" tactic in the monad.
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 |