diff options
author | 2009-08-06 19:00:11 +0000 | |
---|---|---|
committer | 2009-08-06 19:00:11 +0000 | |
commit | ffa57bae1e18fd52d63e8512a352ac63db15a7a9 (patch) | |
tree | 6cf537ce557f14f71ee3693d98dc20c12b64a9e4 /pretyping/termops.ml | |
parent | da7fb3e13166747b49cdf1ecfad394ecb4e0404a (diff) |
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
(uniformisation of function names, classification). One of the most
visible change is the renaming of section_path into full_path (the
use of name section was obsolete due to the module system, but I
don't know if the new name is the best chosen one - especially it
remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r-- | pretyping/termops.ml | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index b7a4fc925..4034d8667 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -34,7 +34,7 @@ let pr_name = function | Name id -> pr_id id | Anonymous -> str "_" -let pr_sp sp = str(string_of_kn sp) +let pr_path sp = str(string_of_kn sp) let pr_con sp = str(string_of_con sp) let rec pr_constr c = match kind_of_term c with @@ -65,9 +65,9 @@ let rec pr_constr c = match kind_of_term c with (str"Evar#" ++ int e ++ str"{" ++ prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") | Const c -> str"Cst(" ++ pr_con c ++ str")" - | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")" + | Ind (sp,i) -> str"Ind(" ++ pr_path sp ++ str"," ++ int i ++ str")" | Construct ((sp,i),j) -> - str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" + str"Constr(" ++ pr_path sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" | Case (ci,p,c,bl) -> v 0 (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++ pr_constr c ++ str"of") ++ cut() ++ @@ -711,7 +711,7 @@ let add_vname vars = function Name id -> Idset.add id vars | _ -> vars -let id_of_global = Nametab.id_of_global +let basename_of_global = Nametab.basename_of_global let sort_hdchar = function | Prop(_) -> "P" @@ -731,9 +731,9 @@ let hdchar env c = if i=0 then lowercase_first_char (id_of_label (label kn)) else - lowercase_first_char (id_of_global (IndRef x)) + lowercase_first_char (basename_of_global (IndRef x)) | Construct ((sp,i) as x) -> - lowercase_first_char (id_of_global (ConstructRef x)) + lowercase_first_char (basename_of_global (ConstructRef x)) | Var id -> lowercase_first_char id | Sort s -> sort_hdchar s | Rel n -> @@ -839,14 +839,14 @@ let is_imported_ref = function let is_global id = try - let ref = locate (make_short_qualid id) in + let ref = locate (qualid_of_ident id) in not (is_imported_ref ref) with Not_found -> false let is_constructor id = try - match locate (make_short_qualid id) with + match locate (qualid_of_ident id) with | ConstructRef _ as ref -> not (is_imported_ref ref) | _ -> false with Not_found -> @@ -907,12 +907,12 @@ let occur_rel p env id = let occur_id nenv id0 c = let rec occur n c = match kind_of_term c with | Var id when id=id0 -> raise Occur - | Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur + | Const kn when basename_of_global (ConstRef kn) = id0 -> raise Occur | Ind ind_sp - when id_of_global (IndRef ind_sp) = id0 -> + when basename_of_global (IndRef ind_sp) = id0 -> raise Occur | Construct cstr_sp - when id_of_global (ConstructRef cstr_sp) = id0 -> + when basename_of_global (ConstructRef cstr_sp) = id0 -> raise Occur | Rel p when p>n & occur_rel (p-n) nenv id0 -> raise Occur | _ -> iter_constr_with_binders succ occur n c |