From 7538094f141ae6fbb6f6e0215e2f405aba1d011b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 12 Jan 2026 10:35:56 +0100 Subject: [PATCH] Improve error message in to-assumption rewrite Currently, if the top-assumption is not an hypothesis, we let an low-tactic error message do escape. We now write a proper error message before this happens. --- src/ecHiGoal.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index f08413545..b16b7eb03 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -1515,8 +1515,12 @@ let rec process_mintros_1 ?(cf = true) ttenv pis gs = and intro1_rw (_ : ST.state) (o, s) tc = let h = EcIdent.create "_" in let rwt tc = - let pt = PT.pt_of_hyp !!tc (FApi.tc1_hyps tc) h in - process_rewrite1_core ~close:false (s, None, o) pt tc + match LDecl.by_id h (FApi.tc1_hyps tc) with + | LD_hyp _ -> + let pt = PT.pt_of_hyp !!tc (FApi.tc1_hyps tc) h in + process_rewrite1_core ~close:false (s, None, o) pt tc + | _ -> + tc_error !!tc "top assumption is not an hypothesis"; in t_seqs [t_intros_i [h]; rwt; t_clear h] tc and intro1_unfold (_ : ST.state) (s, o) p tc =