diff options
| -rw-r--r-- | interp/constrextern.ml | 5 | ||||
| -rwxr-xr-x | library/nametab.ml | 4 | ||||
| -rwxr-xr-x | library/nametab.mli | 2 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 8 |
4 files changed, 11 insertions, 8 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a3c2a0447..1430bdace 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1333,7 +1333,8 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function subst in insert_pat_delimiters (make_pat_notation loc ntn l) key) | SynDefRule kn -> - CPatAtom (loc,Some (Qualid (loc, shortest_qualid_of_syndef kn))) + let qid = shortest_qualid_of_syndef vars kn in + CPatAtom (loc,Some (Qualid (loc, qid))) with No_match -> extern_symbol_pattern allscopes vars t rules @@ -1747,7 +1748,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function subst in insert_delimiters (make_notation loc ntn l) key) | SynDefRule kn -> - CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in + CRef (Qualid (loc, shortest_qualid_of_syndef vars kn)) in if args = [] then e else (* TODO: compute scopt for the extra args, in case, head is a ref *) diff --git a/library/nametab.ml b/library/nametab.ml index ddd06c0c2..e4a8ee995 100755 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -472,9 +472,9 @@ let shortest_qualid_of_global ctx ref = let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in SpTab.shortest_qualid ctx sp !the_ccitab -let shortest_qualid_of_syndef kn = +let shortest_qualid_of_syndef ctx kn = let sp = sp_of_syntactic_definition kn in - SpTab.shortest_qualid Idset.empty sp !the_ccitab + SpTab.shortest_qualid ctx sp !the_ccitab let shortest_qualid_of_module mp = let dir = MPmap.find mp !the_modrevtab in diff --git a/library/nametab.mli b/library/nametab.mli index 81e7c6166..2f6e9e8cb 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -144,7 +144,7 @@ val full_name_module : qualid -> dir_path val sp_of_syntactic_definition : kernel_name -> section_path val shortest_qualid_of_global : Idset.t -> global_reference -> qualid -val shortest_qualid_of_syndef : kernel_name -> qualid +val shortest_qualid_of_syndef : Idset.t -> kernel_name -> qualid val shortest_qualid_of_tactic : ltac_constant -> qualid val dir_of_mp : module_path -> dir_path diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 13d6a62b4..5092601fb 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -203,8 +203,10 @@ let print_located_qualid ref = let (loc,qid) = qualid_of_reference ref in let module N = Nametab in let expand = function - | TrueGlobal ref -> Term ref, N.shortest_qualid_of_global Idset.empty ref - | SyntacticDef kn -> Syntactic kn, N.shortest_qualid_of_syndef kn in + | TrueGlobal ref -> + Term ref, N.shortest_qualid_of_global Idset.empty ref + | SyntacticDef kn -> + Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in match List.map expand (N.extended_locate_all qid) with | [] -> let (dir,id) = repr_qualid qid in @@ -352,7 +354,7 @@ let print_constant_with_infos sp = let print_inductive sp = (print_mutual sp) let print_syntactic_def sep kn = - let qid = Nametab.shortest_qualid_of_syndef kn in + let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn in let c = Syntax_def.search_syntactic_definition dummy_loc kn in (str (if !Options.v7 then "Syntactic Definition " else "Notation ") ++ pr_qualid qid ++ str sep ++ |