From 60de53d159c85b8300226a61aa502a7e0dd2f04b Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 26 Feb 2013 18:52:24 +0000
Subject: kernel/declarations becomes a pure mli

 - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
 - the functions that were in declarations.ml (mostly substitution utilities
   and hashcons) are now in kernel/declareops.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16250 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_typing.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b566dd8afa..b24deb0dc6 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -105,12 +105,12 @@ and check_with_def env sign (idl,c) mp equiv =
 			(union_constraints cb.const_constraints cst1)
 			cst2
 		    in
-		    let def = Def (Declarations.from_val j.uj_val) in
+		    let def = Def (Lazyconstr.from_val j.uj_val) in
 		    def,cst
 		| Def cs ->
-		    let cst1 = Reduction.conv env' c (Declarations.force cs) in
+		    let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
 		    let cst = union_constraints cb.const_constraints cst1 in
-		    let def = Def (Declarations.from_val c) in
+		    let def = Def (Lazyconstr.from_val c) in
 		    def,cst
 	      in
 	      let cb' =
-- 
cgit v1.2.3