From 759e049e8322c90e9cb9b511167d06e49f81818e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 17 Dec 2018 19:21:07 +0100
Subject: Fix #9240: Register for IDProp causes anomaly when non constant

---
 pretyping/evarconv.ml | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3