diff options
Diffstat (limited to 'pretyping/syntax_def.ml')
| -rw-r--r-- | pretyping/syntax_def.ml | 44 |
1 files changed, 22 insertions, 22 deletions
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index f13f31de0..dc5824dc7 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -11,6 +11,7 @@ open Util open Pp open Names +open Libnames open Rawterm open Libobject open Lib @@ -18,51 +19,50 @@ open Nameops (* Syntactic definitions. *) -let syntax_table = ref (Spmap.empty : rawconstr Spmap.t) +let syntax_table = ref (KNmap.empty : rawconstr KNmap.t) let _ = Summary.declare_summary "SYNTAXCONSTANT" { Summary.freeze_function = (fun () -> !syntax_table); Summary.unfreeze_function = (fun ft -> syntax_table := ft); - Summary.init_function = (fun () -> syntax_table := Spmap.empty); + Summary.init_function = (fun () -> syntax_table := KNmap.empty); Summary.survive_section = false } -let add_syntax_constant sp c = - syntax_table := Spmap.add sp c !syntax_table +let add_syntax_constant kn c = + syntax_table := KNmap.add kn c !syntax_table -let cache_syntax_constant (sp,c) = +let cache_syntax_constant ((sp,kn),c) = if Nametab.exists_cci sp then errorlabstrm "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); - add_syntax_constant sp c; - Nametab.push_syntactic_definition sp; - Nametab.push_short_name_syntactic_definition sp + add_syntax_constant kn c; + Nametab.push_syntactic_definition (Nametab.Until 1) sp kn -let load_syntax_constant (sp,c) = +let load_syntax_constant i ((sp,kn),c) = if Nametab.exists_cci sp then errorlabstrm "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); - add_syntax_constant sp c; - Nametab.push_syntactic_definition sp + add_syntax_constant kn c; + Nametab.push_syntactic_definition (Nametab.Until i) sp kn -let open_syntax_constant (sp,c) = - Nametab.push_short_name_syntactic_definition sp +let open_syntax_constant i ((sp,kn),c) = + Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn + +let subst_syntax_constant ((sp,kn),subst,c) = + subst_raw subst c + +let classify_syntax_constant (_,c) = Substitute c let (in_syntax_constant, out_syntax_constant) = - let od = { + declare_object {(default_object "SYNTAXCONSTANT") with cache_function = cache_syntax_constant; load_function = load_syntax_constant; open_function = open_syntax_constant; + subst_function = subst_syntax_constant; + classify_function = classify_syntax_constant; export_function = (fun x -> Some x) } - in - declare_object ("SYNTAXCONSTANT", od) let declare_syntactic_definition id c = let _ = add_leaf id (in_syntax_constant c) in () -let search_syntactic_definition sp = Spmap.find sp !syntax_table - -let locate_syntactic_definition qid = - match Nametab.extended_locate qid with - | Nametab.SyntacticDef sp -> sp - | _ -> raise Not_found +let search_syntactic_definition kn = KNmap.find kn !syntax_table |