Merge PR #9241: Fix #9240: Register for IDProp causes anomaly when non constant

2 files changed, 15 insertions, 8 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e6e1530e36..ed28cc7725 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -46,15 +46,10 @@ let () = Goptions.(declare_bool_option {
 (* Functions to deal with impossible cases *)
 (*******************************************)
 let impossible_default_case env =
-  let type_of_id =
-    let open Names.GlobRef in
-    match Coqlib.lib_ref "core.IDProp.type" with
-    | ConstRef c -> c
-    | VarRef _ | IndRef _ | ConstructRef _ -> assert false
-  in
+  let type_of_id = Coqlib.lib_ref "core.IDProp.type" in
   let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in
-  let (_, u) = Constr.destConst c in
-  Some (c, Constr.mkConstU (type_of_id, u), ctx)
+  let (_, u) = Constr.destRef c in
+  Some (c, Constr.mkRef (type_of_id, u), ctx)
 
 let coq_unit_judge =
   let open Environ in
diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v
new file mode 100644
index 0000000000..e0901dc2d9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9240.v
@@ -0,0 +1,12 @@
+Register unit as core.IDProp.type.
+Register tt as core.IDProp.idProp.
+
+
+Inductive vec (A : Type) : nat -> Type :=
+| nil : vec A 0
+| cons : forall n : nat, A -> vec A n -> vec A (S n).
+
+Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A :=
+match v in (vec _ (S n)) return A with
+| cons _ _ h _ => h
+end. (* assertion failure in evarconv *)