diff options
| author | Pierre-Marie Pédrot | 2014-01-06 14:39:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-06 14:39:53 +0100 |
| commit | 2f6e3a8a453c3fa29bbc660a929c5140916c76b3 (patch) | |
| tree | c7ab6e7576cbbb4adde5404183c062ef697a7389 /tactics | |
| parent | 0427f99bd793a8aa8245e61ec340ca4c6966ba63 (diff) | |
Algebraized "No such hypothesis" errors
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
3 files changed, 3 insertions, 4 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index da8f2668b8..c5017ac75b 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -124,7 +124,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas = match Tacmach.pf_hyps gl with (last_hyp_id,_,_)::_ -> last_hyp_id | _ -> (* even the hypothesis id is missing *) - error ("No such hypothesis: " ^ (Id.to_string !id) ^".") + raise (Logic.RefinerError (Logic.NoSuchHyp !id)) in let gl' = Proofview.V82.of_tactic (general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false) gl in let gls = gl'.Evd.it in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 712191a736..4f7a6188a7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -350,8 +350,7 @@ let interp_hyp ist env (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else user_err_loc (loc,"eval_variable", - str "No such hypothesis: " ++ pr_id id ++ str ".") + else Loc.raise loc (Logic.RefinerError (Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env (loc,id as x) = try coerce_to_hyp_list env (Id.Map.find id ist.lfun) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8546b03a17..be6461de1a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -523,7 +523,7 @@ let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac = aux [] let rec get_next_hyp_position id = function - | [] -> error ("No such hypothesis: " ^ Id.to_string id) + | [] -> raise (RefinerError (NoSuchHyp id)) | (hyp,_,_) :: right -> if Id.equal hyp id then match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast |