diff options
| author | filliatr | 1999-09-10 14:00:56 +0000 |
|---|---|---|
| committer | filliatr | 1999-09-10 14:00:56 +0000 |
| commit | 2c6002d1fbf08ee68914227e3a4267cb38ff8b81 (patch) | |
| tree | 83caeab0f53e7b4fc72ffb1637a0696f0231a2ed /kernel | |
| parent | 540bd2b46fd848fbf6d1f8c2804580d3afed98a6 (diff) | |
modules System, Lib et States
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@71 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 4 | ||||
| -rw-r--r-- | kernel/names.mli | 3 | ||||
| -rw-r--r-- | kernel/reduction.ml | 2 | ||||
| -rw-r--r-- | kernel/typing.ml | 3 |
4 files changed, 8 insertions, 4 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index af07ba426f..6e5835fbb1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -55,7 +55,7 @@ let print_id { atom = a; index = n } = | ("",n) -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >] | (s,n) -> [< 'sTR s ; (if n = (-1) then [< >] else [< 'iNT n >]) >] -let pr_idl idl = prlist_with_sep pr_spc print_id idl +let print_idl idl = prlist_with_sep pr_spc print_id idl let id_ord id1 id2 = let (s1,n1) = repr_ident id1 @@ -168,6 +168,8 @@ let path_of_string s = with | Invalid_argument _ -> invalid_arg "path_of_string" +let print_sp sp = [< 'sTR (string_of_path sp) >] + let coerce_path k { dirpath = p; basename = id } = { dirpath = p; basename = id; kind = k } diff --git a/kernel/names.mli b/kernel/names.mli index be26f0f323..c022a84a3f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -16,7 +16,7 @@ val id_of_string : string -> identifier val explode_id : identifier -> string list val print_id : identifier -> std_ppcmds -val pr_idl : identifier list -> std_ppcmds +val print_idl : identifier list -> std_ppcmds val atompart_of_id : identifier -> string val index_of_id : identifier -> int val id_ord : identifier -> identifier -> int @@ -51,6 +51,7 @@ val kind_of_path : section_path -> path_kind val path_of_string : string -> section_path val string_of_path : section_path -> string val string_of_path_mind : section_path -> identifier -> string +val print_sp : section_path -> std_ppcmds val coerce_path : path_kind -> section_path -> section_path val fwsp_of : section_path -> section_path diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 1e72c40334..f16fa0d8cc 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -160,7 +160,7 @@ let subst_term_occ locs c t = (occ,[]) cl in (occ',DLAMV(n,Array.of_list (List.rev cl') )) - | _ -> occ,t + | _ -> occ,t in if locs = [] then subst_term c t diff --git a/kernel/typing.ml b/kernel/typing.ml index f3928b2fdc..7cd127cf60 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -159,7 +159,8 @@ and execute_array mf env v = (Array.of_list jl, u1) and execute_list mf env = function - | [] -> ([], universes env) + | [] -> + ([], universes env) | c::r -> let (j,u') = execute mf env c in let (jr,u'') = execute_list mf (set_universes u' env) r in |