tmMkInductive should not be used in a tactic

yforster · Dec 19, 2024 · 3f7ea00 · 3f7ea00
1 parent 5672294
commit 3f7ea00
Showing 1 changed file with 7 additions and 4 deletions.
diff --git 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