From e2f27dfcb21c42b72cf8d6a1363251f4c48789cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 5 Mar 2014 12:06:17 +0100
Subject: Changing Retrokwnoledge entry type from kind_of_term to constr. It
 seems it had no particular purpose.

---
 pretyping/vnorm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 8269674d7c..b2fa631cd8 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -71,7 +71,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 Retroknowledge.get_vm_decompile_constant_info env (Ind ind) tag),
+      ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd 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