diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 21:32:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-22 21:32:03 +0000 |
| commit | 937ca7a6dbc1a031b7c4540c665b8774440c1bb9 (patch) | |
| tree | 3a2c73669cb40011c2e62a11d3364d39f74040ba /kernel | |
| parent | de9150e6033467fd2fa8fc93d5f057e8c2f6537f (diff) | |
Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de 'section_path' pour les noms absolus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.ml | 9 | ||||
| -rw-r--r-- | kernel/names.mli | 11 | ||||
| -rw-r--r-- | kernel/type_errors.ml | 2 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 2 |
4 files changed, 22 insertions, 2 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 8205c564e..76f17525d 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -126,6 +126,15 @@ let kind_of_string = function | "obj" -> OBJ | _ -> invalid_arg "kind_of_string" +(*s Section paths *) + +type qualid = string list * string + +let make_qualid p s = (p,s) +let repr_qualid q = q + +let string_of_qualid (l,s) = String.concat "." (l@[s]) +let print_qualid (l,s) = prlist_with_sep (fun () -> pr_str ".") pr_str (l@[s]) (*s Section paths *) diff --git a/kernel/names.mli b/kernel/names.mli index 323009011..3a380a42d 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -49,6 +49,17 @@ type dir_path = string list (* Printing of directory paths as ["#module#submodule"] *) val string_of_dirpath : dir_path -> string + +(*s Section paths *) + +type qualid + +val make_qualid : string list -> string -> qualid +val repr_qualid : qualid -> string list * string + +val string_of_qualid : qualid -> string +val print_qualid : qualid -> std_ppcmds + (*s Section paths *) type section_path diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index a79dbcf3c..39223c726 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -60,7 +60,7 @@ type type_error = | WrongPredicateArity of constr * int * int | NeedsInversion of constr * constr (* Relocation error *) - | GlobalNotFound of section_path + | QualidNotFound of qualid exception TypeError of path_kind * env * type_error diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 9a2504ff8..68628c63c 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -64,7 +64,7 @@ type type_error = | WrongPredicateArity of constr * int * int | NeedsInversion of constr * constr (* Relocation error *) - | GlobalNotFound of section_path + | QualidNotFound of qualid exception TypeError of path_kind * env * type_error |