From 2ec78477c720ba3a5343b49f25cfa9c1639adbba Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Fri, 7 Sep 2018 17:34:11 +0200
Subject: Retroknowledge: use GlobRef.t instead of Constr.t as entry

---
 pretyping/nativenorm.ml | 2 +-
 pretyping/vnorm.ml      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 246acfc92e..20185363e6 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   try
     if const then
       let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
-      Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp
+      Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag, ctyp
     else
       raise Not_found
   with Not_found ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 255707dc7b..266e94b34d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -79,7 +79,7 @@ let construct_of_constr const env tag typ =
   (* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
   try
     if const then
-      ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag),
+      ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag),
        typ) (*spiwack: this may need to be changed in case there are parameters in the
 	               type which may cause a constant value to have an arity.
 	               (type_constructor seems to be all about parameters actually)
-- 
cgit v1.2.3