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 /stm | |
| parent | dc8750d166cffd846619d2de20e02a4e31c6357f (diff) | |
Put the "fix" tactic in the monad.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 80b3fef196..8db8de9927 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 -> Tactics.mutual_cofix id l 0 + | (id,_)::l -> Proofview.V82.tactic (Tactics.mutual_cofix id l 0) | _ -> assert false else (* nl is dummy: it will be recomputed at Qed-time *) @@ -403,7 +403,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = | Anonymous -> Tactics.intro) (List.rev ids) in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> - let rec_tac = Proofview.V82.tactic (rec_tac_initializer finite guard thms snl) in + let rec_tac = rec_tac_initializer finite guard thms snl in Some (match init_tac with | None -> if Flags.is_auto_intros () then |