diff options
| author | herbelin | 2003-09-12 14:40:51 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-12 14:40:51 +0000 |
| commit | 7dfc58207fc6a1eb50841640fb26aa8e32ca17c7 (patch) | |
| tree | f2ca4a2f44dfe8c7fe150acc6a3f00380f6f706d /interp | |
| parent | d78ac151793dc8df15e7e687e5e20d5f48cd53d1 (diff) | |
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
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 -> |