diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretype_errors.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 2 | ||||
| -rw-r--r-- | pretyping/syntax_def.ml | 2 | ||||
| -rw-r--r-- | pretyping/syntax_def.mli | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 594f3fc9e..3a6897d98 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -13,8 +13,8 @@ let raise_pretype_error (loc,k,ctx,te) = let error_var_not_found_loc loc k s = raise_pretype_error (loc,k, Global.env() (*bidon*), VarNotFound s) -let error_global_not_found_loc loc sp = - raise_pretype_error (loc,CCI, Global.env() (*bidon*), GlobalNotFound sp) +let error_global_not_found_loc loc q = + raise_pretype_error (loc,CCI, Global.env() (*bidon*), QualidNotFound q) let error_cant_find_case_type_loc loc env expr = raise_pretype_error (loc, CCI, env, CantFindCaseType expr) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index c670e1f97..e91ec8a45 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -17,7 +17,7 @@ val error_var_not_found_loc : loc -> path_kind -> identifier -> 'a val error_global_not_found_loc : - loc -> section_path -> 'a + loc -> qualid -> 'a val error_cant_find_case_type_loc : loc -> env -> constr -> 'a diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index 0038b69d5..f90627f7e 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -35,7 +35,7 @@ let (in_syntax_constant, out_syntax_constant) = let _ = cache_syntax_constant := fun (sp,c) -> add_syntax_constant sp c; - Nametab.push_obj (basename sp) (sp, in_syntax_constant c) + Nametab.push_object (basename sp) (sp, in_syntax_constant c) let declare_syntactic_definition id c = let _ = add_leaf id CCI (in_syntax_constant c) in () diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli index 48a996991..7a1116ba0 100644 --- a/pretyping/syntax_def.mli +++ b/pretyping/syntax_def.mli @@ -12,6 +12,6 @@ val declare_syntactic_definition : identifier -> rawconstr -> unit val search_syntactic_definition : section_path -> rawconstr -val locate_syntactic_definition : section_path -> section_path +val locate_syntactic_definition : qualid -> section_path |