diff options
Diffstat (limited to 'plugins/subtac/subtac_utils.ml')
| -rw-r--r-- | plugins/subtac/subtac_utils.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index fbe40525b..64f5fe9c7 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -323,7 +323,7 @@ let and_tac l hook = aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl in let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in - Command.start_proof and_proofid goal_kind and_goal + Lemmas.start_proof and_proofid goal_kind and_goal (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract)); trace (str "Started and proof"); Pfedit.by and_tac; |