diff options
Diffstat (limited to 'pretyping')
| -rwxr-xr-x | pretyping/classops.ml | 3 | ||||
| -rw-r--r-- | pretyping/syntax_def.ml | 42 |
2 files changed, 28 insertions, 17 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 8cbfcc0a5b..556dbd3341 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -14,6 +14,7 @@ open Options open Names open Environ open Libobject +open Library open Declare open Term open Rawterm @@ -30,7 +31,7 @@ let cte_of_constr c = match kind_of_term c with | IsConst (sp,_) -> ConstRef sp | IsMutInd (ind_sp,_) -> IndRef ind_sp | IsMutConstruct (cstr_cp,_) -> ConstructRef cstr_cp - | IsVar id -> VarRef (find_section_variable id) + | IsVar id -> VarRef (Declare.find_section_variable id) | _ -> raise Not_found type cl_typ = diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index 6a171d7c46..1b875affa7 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -8,6 +8,8 @@ (* $Id$ *) +open Util +open Pp open Names open Rawterm open Libobject @@ -27,31 +29,39 @@ let _ = Summary.declare_summary let add_syntax_constant sp c = syntax_table := Spmap.add sp c !syntax_table -(* Impossible de rendre récursive la définition de in_syntax_constant - et cache_syntax_constant, alors on triche ... *) -let cache_syntax_constant = ref (fun c -> failwith "Undefined function") +let cache_syntax_constant (sp,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 + +let load_syntax_constant (sp,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 + +let open_syntax_constant (sp,c) = + Nametab.push_short_name_syntactic_definition sp let (in_syntax_constant, out_syntax_constant) = let od = { - cache_function = (fun c -> !cache_syntax_constant c); - load_function = (fun _ -> ()); - open_function = (fun c -> !cache_syntax_constant c); + cache_function = cache_syntax_constant; + load_function = load_syntax_constant; + open_function = open_syntax_constant; export_function = (fun x -> Some x) } in declare_object ("SYNTAXCONSTANT", od) -let _ = - cache_syntax_constant := fun (sp,c) -> - add_syntax_constant sp c; - Nametab.push_object sp (in_syntax_constant c) - let declare_syntactic_definition id c = let _ = add_leaf id CCI (in_syntax_constant c) in () let search_syntactic_definition sp = Spmap.find sp !syntax_table -let locate_syntactic_definition sp = - let (sp,obj) = Nametab.locate_obj sp in - if object_tag obj = "SYNTAXCONSTANT" then sp else raise Not_found - - +let locate_syntactic_definition qid = + match Nametab.extended_locate qid with + | Nametab.SyntacticDef sp -> sp + | _ -> raise Not_found |