Unquoting constant with wrong modpath raises anomaly

[yforster]

From MetaCoq.Template Require Import All.
Require Import List String.
Import ListNotations.

MetaCoq Run (tmUnquoteTyped nat ((tConstruct (mkInd (MPfile ["Wrong"], "nat") 0) 0 []))).

results in

Error: Anomaly "File "clib/int.ml", line 46, characters 14-20: Assertion failed."
Please report at http://coq.inria.fr/bugs/.

on the 8.12 branch, and also on the 8.11 branch, meaning it's probably a real bug which was there before and not introduced by me while porting. @SimonBoulier can you have a look?

[SimonBoulier]

Isn't the expected behavior?

[yforster]

I would say the expected behaviour is an error which says "constant Wrong.nat not found" or something similar. I'm particularly worried about the word "anomaly" occurring, we don't want people to file a Coq bug here.

[SimonBoulier]

Hum. I see. Not sure how easy it is to fix this.