diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:37 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-29 10:48:37 +0000 |
commit | 32170384190168856efeac5bcf90edf1170b54d6 (patch) | |
tree | 0ea86b672df93d997fa1cab70b678ea7abdcf171 /library/nametab.ml | |
parent | 1e5182e9d5c29ae9adeed20dae32969785758809 (diff) |
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2722 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.ml')
-rwxr-xr-x | library/nametab.ml | 32 |
1 files changed, 28 insertions, 4 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index 99524bde1..b28506f91 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -139,6 +139,8 @@ let push_idtree extract_dirpath tab n dir id o = let push_long_names_ccipath = push_idtree dirpath_of_extended_ref the_ccitab let push_short_name_ccipath = push_idtree dirpath_of_extended_ref the_ccitab +let push_long_names_objpath = + push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab let push_short_name_objpath = push_idtree (fun sp -> let (p,_) = repr_path sp in p) the_objtab @@ -181,6 +183,12 @@ let push_short_name_object sp = let _, s = repr_qualid (qualid_of_sp sp) in push_short_name_objpath 0 empty_dirpath s sp +(* This is for tactic definition names *) + +let push_tactic_path sp = + let dir, s = repr_qualid (qualid_of_sp sp) in + push_long_names_objpath 0 dir s sp + (* This is to remember absolute Section/Module names and to avoid redundancy *) let push_section fulldir = let dir, s = split_dirpath fulldir in @@ -213,6 +221,10 @@ let locate_obj qid = let (dir,id) = repr_qualid qid in locate_in_tree (Idmap.find id !the_objtab) dir +let locate_tactic qid = + let (dir,id) = repr_qualid qid in + locate_in_tree (Idmap.find id !the_objtab) dir + (* Actually, this table has only two levels, since only basename and *) (* fullname are registered *) let push_loaded_library fulldir = @@ -259,13 +271,13 @@ let absolute_reference sp = let locate_in_absolute_module dir id = absolute_reference (make_path dir id) -let global loc qid = +let global (loc,qid) = try match extended_locate qid with | TrueGlobal ref -> ref | SyntacticDef _ -> - error - ("Unexpected reference to a syntactic definition: " - ^(string_of_qualid qid)) + user_err_loc (loc,"global", + str "Unexpected reference to a syntactic definition: " ++ + pr_qualid qid) with Not_found -> error_global_not_found_loc loc qid @@ -299,6 +311,13 @@ let pr_global_env env ref = let s = string_of_qualid (shortest_qualid_of_global env ref) in (str s) +let global_inductive (loc,qid as locqid) = + match global locqid with + | IndRef ind -> ind + | ref -> + user_err_loc (loc,"global_inductive", + pr_qualid qid ++ spc () ++ str "is not an inductive type") + (********************************************************************) (********************************************************************) @@ -330,3 +349,8 @@ let _ = Summary.unfreeze_function = unfreeze; Summary.init_function = init; Summary.survive_section = false } + +type strength = + | NotDeclare + | DischargeAt of dir_path * int + | NeverDischarge |