diff options
| author | Pierre-Marie Pédrot | 2016-05-16 21:21:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 21:36:08 +0200 |
| commit | a4bd166bd2119a5290276f0ded44f8186ba1ecee (patch) | |
| tree | a99e711e613edb17d3172a3bbf9f178a6e8a9019 /ltac | |
| parent | 1394bab8ba40dd4714e941586109fd88a79ef653 (diff) | |
Put the "cofix" 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 4893e40973..766f0714d2 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -238,8 +238,8 @@ END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ] -| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ] + [ "cofix" ] -> [ Tactics.cofix None ] +| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ] END (* Clear *) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 7acdff9acf..5aff262aa5 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1729,7 +1729,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_cofix (interp_ident ist env sigma id) l_interp 0) in + let tac = Tactics.mutual_cofix (interp_ident ist env sigma id) l_interp 0 in Sigma.Unsafe.of_pair (tac, sigma) end } end |