`Unquote Definition` will normalize the term

[WeituoDAI]

Unquote Definition will normalize the term automatically,
An example:

MetaCoq Quote Definition mytp := (fun (x:nat) => x) 1.
MetaCoq Unquote Definition mytp' := mytp.
Print mytp'.

The output is mytp' = 1 : nat. Not the same as originally defined.
I wonder if this is the expected behavior. I hope that I can get the original definition but not the term after normalization.

The problem possibly comes from tmEval.
When use tmUnquote to the term mytp, I get {| my_projT1 := nat; my_projT2 := (fun x:nat => x) 1 |}.
Then use tmEval cbv/cbn/unfold ... on the term my_projT2 {| my_projT1 := nat; my_projT2 := (fun x:nat => x) 1 |}, we will always beta-reduce the term.

I define my own plugin to get the (non normalized) unquoted term:

Notation "'$let' x ':=' c1 'in' c2" := (@bind _ _ _ _ c1 (fun x => c2))
  (at level 100, c1 at next level, right associativity, x pattern) : monad_scope.
Definition MyDef (a : term) (out : option ident): TemplateMonad unit :=
  $let b := tmUnquote a in
  let ty := my_projT1 b in
  $let r := tmUnquoteTyped ty a in
  match out with
  | Some name => tmDefinitionRed name (Some all) r ;; tmPrint r ;; ret tt
  | None => tmPrint r
  end.

However, this function does unquotation twice.. It will help if there is any better approach to do this. Anyway, I do not think that MetaCoq Unquote Definition should normalize the term.