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 /stm | |
| parent | 1394bab8ba40dd4714e941586109fd88a79ef653 (diff) | |
Put the "cofix" tactic in the monad.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 8db8de9927..ce5ef01699 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -385,7 +385,7 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_ let rec_tac_initializer finite guard thms snl = if finite then match List.map (fun ((id,_),(t,_)) -> (id,t)) thms with - | (id,_)::l -> Proofview.V82.tactic (Tactics.mutual_cofix id l 0) + | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else (* nl is dummy: it will be recomputed at Qed-time *) |