(
let newhypo = status_parameter "volatile_newhypo" status in
if newhypo = "" then
- fail (lazy "Invalid use of 'or equivalently'")
+ fail (lazy "Invalid use of 'that is equivalent to'")
else
change_tac ~where:("",0,(None,[newhypo,Ast.UserInput],None)) ~with_what:t status
)
[] -> []
| hd :: tl -> if n = 0 then [] else hd :: (sublist (n-1) tl)
in
- List.map (fun _,sw -> goal_of_switch sw) (sublist (List.length !cl) g)
+ List.map (fun (_,sw) -> goal_of_switch sw) (sublist (List.length !cl) g)
in
let rec add_names_to_goals g cl metasenv =
match g,cl with
| FirstTypeWrong -> fail (lazy "What you want to prove is different from the conclusion")
;;
-let byinduction t1 id = suppose t1 id ;;
+let byinduction t1 id status =
+ let ctx = status_parameter "context" status in
+ if ctx <> "induction" then fail (lazy "You can't use this tactic outside of an induction context")
+ else suppose t1 id status
+;;
let name_of_conj conj =
let mattrs,_,_ = conj in
let loc =
try
loc_of_goal goal_to_focus t
- with _ -> fail (lazy "The given case is not part of the current induction/cases analysis
- context")
+ with _ -> fail (lazy "The given case is not part of the current induction/cases analysis context")
in
let curloc = if has_focused_goal status then
let goal = extract_first_goal_from_status status in
let case id l status =
let ctx = status_parameter "context" status in
- if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an
- induction/cases analysis context")
+ if ctx <> "induction" && ctx <> "cases" then fail (lazy "You can't use case outside of an induction/cases analysis context")
else
(
if has_focused_goal status then fail (lazy "Finish the current case before switching")