diff options
Diffstat (limited to 'toplevel/lemmas.ml')
| -rw-r--r-- | toplevel/lemmas.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 91886e076..20b792cc0 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -300,7 +300,7 @@ let start_proof id kind c ?init_tac ?(compute_guard=[]) hook = let rec_tac_initializer finite guard thms snl = if finite then match List.map (fun (id,(t,_)) -> (id,t)) thms with - | (id,_)::l -> Hiddentac.h_mutual_cofix id l + | (id,_)::l -> Tactics.mutual_cofix id l 0 | _ -> assert false else (* nl is dummy: it will be recomputed at Qed-time *) @@ -308,7 +308,7 @@ let rec_tac_initializer finite guard thms snl = | None -> List.map succ (List.map List.last guard) | Some nl -> nl in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with - | (id,n,_)::l -> Hiddentac.h_mutual_fix id n l + | (id,n,_)::l -> Tactics.mutual_fix id n l 0 | _ -> assert false let start_proof_with_initialization kind recguard thms snl hook = |