From 7dfc58207fc6a1eb50841640fb26aa8e32ca17c7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 14:40:51 +0000
Subject: Scope type pour le codomaine de Prod aussi

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4359 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ce4fb5fe11..b4edaaf1ec 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -116,7 +116,7 @@ let add_glob loc ref =
   i*)
   let sp = Nametab.sp_of_global ref in
   let id = let _,id = repr_path sp in string_of_id id in
-  let dp = string_of_dirpath (Declare.library_part ref) in
+  let dp = string_of_dirpath (Lib.library_part ref) in
   dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id)
 
 (**********************************************************************)
@@ -611,7 +611,7 @@ let internalise sigma env allow_soapp lvar c =
 	let body = iterate_prod loc2 (push_name_env env na) ty body nal in
 	let ty = locate_if_isevar loc1 na (intern_type env ty) in
 	RProd (join_loc loc1 loc2, na, ty, body)
-    | [] -> intern env body
+    | [] -> intern_type env body
 
   and iterate_lam loc2 env ty body = function
     | (loc1,na)::nal ->
-- 
cgit v1.2.3