From 3f7ea005878717e1f0693cd49151b52d552472fa Mon Sep 17 00:00:00 2001 From: Yannick Forster Date: Thu, 19 Dec 2024 16:25:59 +0100 Subject: [PATCH] tmMkInductive should not be used in a tactic --- template-coq/src/run_template_monad.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml index 31c18e127..8d6f0f42e 100644 --- a/template-coq/src/run_template_monad.ml +++ b/template-coq/src/run_template_monad.ml @@ -531,10 +531,13 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co Plugin_core.run ~st (Plugin_core.tmEval red trm) env evm (fun ~st env evm trm -> k ~st env evm (quote_term env evm trm)) | TmMkInductive (b, mind) -> - let infer_univs = unquote_bool (reduce_all env evm b) in - let evm = declare_inductive env evm infer_univs mind in - let env = Global.env () in - k ~st env evm (Lazy.force unit_tt) + if intactic + then not_in_tactic "tmMkInductive" + else + let infer_univs = unquote_bool (reduce_all env evm b) in + let evm = declare_inductive env evm infer_univs mind in + let env = Global.env () in + k ~st env evm (Lazy.force unit_tt) | TmUnquote t -> begin try