diff options
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f90e889678..b60b77595b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -23,7 +23,6 @@ open Names open Nameops open Libnames open Globnames -open Nametab open Refiner open Tacmach.New open Tactic_debug @@ -358,7 +357,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (qualid_of_ident ?loc id) + | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (qualid_of_ident ?loc id)) + Nametab.error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p |