Anomaly when defining and using inductive types while in interactive proof mode.

[DeLectionnes]

It is possible to define inductive types in interactive mode via Ltac.
If those types are not used in the proof term, they are only accessible (e.g. via Print) inside the proof they were defined in, and not outside of it.
If they are used in the Proof term, trying to conclude the proof with Qed causes an anomaly :

Error: Anomaly "Inductive name_of the_inductive does not appear in the environment."
Please report at http://coq.inria.fr/bugs/.

Here is an example code with both phenomena :

Example

From MetaCoq.Template Require Export All Checker Reduction.
From MetaCoq.Utils Require Import utils.

Notation "'$run' f" := ltac:(let p y := exact y in
                             run_template_program
                             f
                             p) (at level 0).


Definition rename_oib (oib : one_inductive_body) : one_inductive_body :=
  {|
    ind_name := oib.(ind_name) ^ "__renamed";
    ind_indices := oib.(ind_indices);
    ind_sort := oib.(ind_sort);
    ind_type :=  oib.(ind_type);
    ind_kelim := oib.(ind_kelim);
    ind_ctors := oib.(ind_ctors);
    ind_projs := oib.(ind_projs);
    ind_relevance := oib.(ind_relevance)
  |}.

Definition rename_mib (mib : mutual_inductive_body) : mutual_inductive_body :=
  {|
    ind_finite := mib.(ind_finite);
    ind_npars :=  mib.(ind_npars);
    ind_params := mib.(ind_params);
    ind_universes := mib.(ind_universes);
    ind_variance := mib.(ind_variance);
    ind_bodies := map (rename_oib) mib.(ind_bodies)
  |}.

Definition rename_ind{X}(R:X): TemplateMonad unit :=
  tmBind (tmQuote R)
   ( fun quote_ind =>
      match quote_ind with
      | tInd ind _ =>
          let ker := inductive_mind ind in
      tmBind (tmQuoteInductive ker)
        (fun mib : mutual_inductive_body => let mib' := rename_mib mib in tmMkInductive' mib')
  | _ => tmFail "erreur"
  end).

MetaCoq Run (rename_ind (@list)).
Print list__renamed.

Definition quote_then_rename{X}(R:X) :=
  tmBind (rename_ind R) (fun _ => tmQuote R).
  
  
Notation "'$quote_bis' x" := ($run (quote_then_rename x)) (at level 0).


Definition ex1: forall n, n = (S n) -> term.
Proof.
  intro n.
  refine (fun _ => $quote_bis nat).
  Print nat__renamed.
Qed.

Fail Print nat__renamed.

Definition temp := fun (t:term)(T:Type) => True.

Definition ex2: forall n, n = (S n) -> Prop.
Proof.
  intro n.
  refine (fun _ => temp ($quote_bis nat) _).
  exact nat__renamed.
  Print nat__renamed.
Qed.