From 937ca7a6dbc1a031b7c4540c665b8774440c1bb9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 22 Nov 2000 21:32:03 +0000
Subject: Abstraction du type 'qualid' pour les noms qualifiés relatifs
 distinct de 'section_path' pour les noms absolus

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretype_errors.ml  | 4 ++--
 pretyping/pretype_errors.mli | 2 +-
 pretyping/syntax_def.ml      | 2 +-
 pretyping/syntax_def.mli     | 2 +-
 4 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 594f3fc9e3..3a6897d98a 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 c670e1f971..e91ec8a45c 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 0038b69d57..f90627f7e9 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 48a996991a..7a1116ba05 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
 
 
-- 
cgit v1.2.3