diff options
| -rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 18 | ||||
| -rw-r--r-- | test-suite/success/ltac.v | 15 | ||||
| -rw-r--r-- | test-suite/success/unfold.v | 8 |
4 files changed, 40 insertions, 8 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8898e5989a..7017edaf28 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -249,6 +249,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct str " depends on pattern variable name " ++ pr_id id ++ str " which is not bound in current context.") + let protected_get_type_of env sigma c = + try Retyping.get_type_of env sigma c + with Anomaly _ -> + errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.") + let pretype_id loc env sigma (lvar,unbndltacvars) id = (* Look for the binder of [id] *) try @@ -260,7 +265,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let (ids,c) = List.assoc id lvar in let subst = List.map (invert_ltac_bound_name env id) ids in let c = substl subst c in - { uj_val = c; uj_type = Retyping.get_type_of env sigma c } + { uj_val = c; uj_type = protected_get_type_of env sigma c } with Not_found -> (* Check if [id] is a section or goal variable *) try diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1957f04751..f067141a8b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -395,8 +395,10 @@ let intern_ltac_variable ist = function raise Not_found let intern_constr_reference strict ist = function - | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist -> - RVar (dloc,id), None + | Ident (_,id) as r when not strict & find_hyp id ist -> + RVar (dloc,id), Some (CRef r) + | Ident (_,id) as r when find_ctxvar id ist -> + RVar (dloc,id), if strict then None else Some (CRef r) | r -> let loc,_ as lqid = qualid_of_reference r in RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) @@ -558,9 +560,10 @@ let intern_evaluable_reference_or_by_notation ist = function (* Globalize a reduction expression *) let intern_evaluable ist = function | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id) - | AN (Ident (_,id)) when - (not !strict_check & find_hyp id ist) or find_ctxvar id ist -> - ArgArg (EvalVarRef id, None) + | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist -> + ArgArg (EvalVarRef id, Some (loc,id)) + | AN (Ident (loc,id)) when find_ctxvar id ist -> + ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in @@ -1132,7 +1135,8 @@ let interp_hyp ist gl (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",pr_id id ++ str " not found.") + else user_err_loc (loc,"eval_variable", + str "No such hypothesis: " ++ pr_id id ++ str ".") let hyp_list_of_VList env = function | VList l -> List.map (coerce_to_hyp env) l @@ -1204,7 +1208,7 @@ let interp_evaluable ist env = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> Pretype_errors.error_var_not_found_loc loc id) + | _ -> error_global_not_found_loc (loc,qualid_of_ident id)) | ArgArg (r,None) -> r | ArgVar locid -> interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index bbaeb08992..32c6d14311 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -266,3 +266,18 @@ reflexivity. f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *) || exact I. Qed. + +(* Test regular failure when clear/intro breaks soundness of the + interpretation of terms in current environment *) + +Ltac g y := clear y; assert (y=y). +Goal forall x:nat, True. +intro x. +Fail g x. +Abort. + +Ltac h y := assert (y=y). +Goal forall x:nat, True. +intro x. +Fail clear x; f x. +Abort. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 47ca0836b5..5649e2f712 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -13,3 +13,11 @@ Goal EQ nat 0 0. Hint Unfold EQ. auto. Qed. + +(* Check regular failure when statically existing ref does not exist + any longer at run time *) + +Goal let x := 0 in True. +intro x. +Fail (clear x; unfold x). +Abort. |