From 1700df5002f7fc2e16c3a8c180cb5d5ead97a390 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 26 Oct 2011 13:17:55 +0000
Subject: Mod_subst: some simplifications, some more significant names to
 functions, etc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14612 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c620d8dd26..c2d71ebb27 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -271,7 +271,7 @@ let add_constant dir l decl senv =
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
-      update_resolver (add_inline_delta_resolver kn lev) senv'
+      update_resolver (add_inline_delta_resolver (user_con kn) (lev,None)) senv'
     | _ -> senv'
   in
   kn, senv''
-- 
cgit v1.2.3