modifs pour premiere edition de liens

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@189 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 53 insertions, 55 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 7dca2b1c8..2305f31ff 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -47,6 +47,7 @@ let _ = Summary.declare_summary "VARIABLE"
 let cache_variable (sp,(id,(ty,_,_) as vd)) = 
   Global.push_var (id,ty);
   Nametab.push id sp;
+  declare_var_implicits id;
   vartab := Spmap.add sp vd !vartab
 
 let load_variable _ = 
@@ -69,16 +70,19 @@ let (in_variable, out_variable) =
 let declare_variable id ((ty,_,_) as obj) =
   Global.push_var (id,ty);
   let sp = add_leaf id CCI (in_variable (id,obj)) in
-  Nametab.push id sp
+  Nametab.push id sp;
+  declare_var_implicits id
 
 (* Parameters. *)
 
 let cache_parameter (sp,c) =
   Global.add_parameter sp c;
-  Nametab.push (basename sp) sp
+  Nametab.push (basename sp) sp;
+  declare_constant_implicits sp
 
 let open_parameter (sp,_) =
-  Nametab.push (basename sp) sp
+  Nametab.push (basename sp) sp;
+  declare_constant_implicits sp
 
 let specification_parameter obj = obj
 
@@ -93,7 +97,8 @@ let (in_parameter, out_parameter) =
 let declare_parameter id c =
   let sp = add_leaf id CCI (in_parameter c) in
   Global.add_parameter sp c;
-  Nametab.push (basename sp) sp
+  Nametab.push (basename sp) sp;
+  declare_constant_implicits sp
  
 (* Constants. *)
 
@@ -169,41 +174,6 @@ let declare_mind mie =
   push_inductive_names sp mie;
   declare_inductive_implicits sp
 
-(* Syntax constants. *)
-
-let syntax_table = ref (Idmap.empty : constr Idmap.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 := Idmap.empty) }
-
-let add_syntax_constant id c =
-  syntax_table := Idmap.add id c !syntax_table
-
-let cache_syntax_constant (sp,c) = 
-  add_syntax_constant (basename sp) c;
-  Nametab.push (basename sp) sp
-
-let open_syntax_constant (sp,_) =
-  Nametab.push (basename sp) sp
-
-let (in_syntax_constant, out_syntax_constant) =
-  let od = {
-    cache_function = cache_syntax_constant;
-    load_function = (fun _ -> ());
-    open_function = open_syntax_constant;
-    specification_function = (fun x -> x) } in
-  declare_object ("SYNTAXCONSTANT", od)
-
-let declare_syntax_constant id c =
-  let sp = add_leaf id CCI (in_syntax_constant c) in
-  add_syntax_constant id c;
-  Nametab.push (basename sp) sp
-
-let out_syntax_constant id = Idmap.find id !syntax_table
-
 (* Test and access functions. *)
 
 let is_constant sp = 
@@ -273,6 +243,8 @@ let global_reference_imps kind id =
 	c, list_of_implicits (constructor_implicits ((sp,i),j))
     | _ -> assert false
 
+let global env id = global_reference CCI id
+
 let is_global id =
   try 
     let osp = Nametab.sp_of_id CCI id in
diff --git a/library/declare.mli b/library/declare.mli
index a8848660d..11f6b2497 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -23,7 +23,6 @@ type strength =
 type variable_declaration = constr * strength * bool
 val declare_variable : identifier -> variable_declaration -> unit
 
-
 type constant_declaration = constant_entry * strength * bool
 val declare_constant : identifier -> constant_declaration -> unit
 
@@ -33,8 +32,6 @@ val declare_mind : mutual_inductive_entry -> unit
 
 val declare_eliminations : section_path -> unit
 
-val declare_syntax_constant : identifier -> constr -> unit
-
 val make_strength : string list -> strength
 val make_strength_0 : unit -> strength
 val make_strength_1 : unit -> strength
@@ -49,7 +46,6 @@ val is_variable : identifier -> bool
 val out_variable : section_path -> identifier * typed_type * strength * bool
 val variable_strength : identifier -> strength
 
-val out_syntax_constant : identifier -> constr
 
 (*s It also provides a function [global_reference] to construct a global
   constr (a constant, an inductive or a constructor) from an identifier.
@@ -61,6 +57,8 @@ val global_operator : section_path -> identifier -> sorts oper * var_context
 val global_reference : path_kind -> identifier -> constr
 val global_reference_imps : path_kind -> identifier -> constr * int list
 
+val global : Environ.env -> identifier -> constr
+
 val is_global : identifier -> bool
 
 val mind_path : constr -> section_path
diff --git a/library/goptions.ml b/library/goptions.ml
index 4f5133226..a54d0870c 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -49,7 +49,7 @@ module MakeTable =
     let kn = nickname A.key
 
     let _ =
-      if List.mem_assoc kn !param_table then 
+      if List.mem_assoc kn !param_table then
 	error "Sorry, this table name is already used"
 
     module MyType = struct type t = A.t let compare = Pervasives.compare end
@@ -81,8 +81,8 @@ module MakeTable =
 		Libobject.open_function = open_options;
 		Libobject.cache_function = cache_options;
 		Libobject.specification_function = specification_options}) in
-        ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))),
-         (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c))))
+        ((fun c -> let _ = Lib.add_anonymous_leaf (inGo (GOadd, c)) in ()),
+         (fun c -> let _ = Lib.add_anonymous_leaf (inGo (GOrmv, c)) in ()))
       else
         ((fun c -> t := MySet.add c !t),
          (fun c -> t := MySet.remove c !t))
@@ -244,8 +244,8 @@ let set_option_value check_and_cast key v =
   in
   match info with
     | Sync  current  ->
-      	Lib.add_anonymous_leaf
-	  (inOptVal (key,(name,check_and_cast v current)))
+      	let _ = Lib.add_anonymous_leaf
+		  (inOptVal (key,(name,check_and_cast v current))) in ()
     | Async (read,write) -> write (check_and_cast v (read ()))
 
 let bad_type_error () = error "Bad type of value for this option"
diff --git a/library/impargs.ml b/library/impargs.ml
index baa993312..819873282 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -91,21 +91,36 @@ let inductive_implicits_list ind_sp =
 let constant_implicits_list sp =
   list_of_implicits (constant_implicits sp)
 
-let implicits_of_var kind id =
-  failwith "TODO: implicits of vars"
+(* Variables. *)
+
+let var_table = ref Idmap.empty
+
+let declare_var_implicits id = 
+  let (_,ty) = Global.lookup_var id in
+  let imps = auto_implicits ty.body in
+  var_table := Idmap.add id imps !var_table
+
+let implicits_of_var _ id =
+  list_of_implicits (Idmap.find id !var_table)
 
 (* Registration as global tables and roolback. *)
 
-type frozen = implicits Spmap.t
+type frozen_t = implicits Spmap.t 
+              * (implicits * implicits array) array Spmap.t 
+              * implicits Idmap.t
 
 let init () =
-  constants_table := Spmap.empty
+  constants_table := Spmap.empty;
+  inductives_table := Spmap.empty;
+  var_table := Idmap.empty
 
 let freeze () =
-  !constants_table
+  !constants_table, !inductives_table, !var_table
 
-let unfreeze ct =
-  constants_table := ct
+let unfreeze (ct,it,vt) =
+  constants_table := ct;
+  inductives_table := it;
+  var_table := vt
 
 let _ = 
   Summary.declare_summary "implicits"
diff --git a/library/impargs.mli b/library/impargs.mli
index 8659b4b40..243eb8031 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -33,5 +33,9 @@ val constructor_implicits_list : constructor_path -> int list
 val inductive_implicits_list : inductive_path -> int list
 val constant_implicits_list : section_path -> int list
 
+val declare_var_implicits : identifier -> unit
 val implicits_of_var : Names.path_kind -> identifier -> int list
 
+type frozen_t
+val freeze : unit -> frozen_t
+val unfreeze : frozen_t -> unit
diff --git a/library/lib.ml b/library/lib.ml
index ea8120787..075e0e12a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -178,6 +178,7 @@ let reset_to sp =
   let (after,_,_) = split_lib spf in
   recache_context (List.rev after)
 
+let is_section_p sp = list_prefix_of (wd_of_sp sp) !path_prefix
 
 (* State and initialization. *)
 
diff --git a/library/lib.mli b/library/lib.mli
index d87c4573a..826cc12e7 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -39,6 +39,7 @@ val close_section : string -> unit
 
 val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> string list
+val is_section_p : section_path -> bool
 
 val open_module : string -> unit
 val export_module : unit -> library_segment
diff --git a/library/states.ml b/library/states.ml
index d8fed1437..be1241a9a 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -23,6 +23,9 @@ let (extern_state,intern_state) =
 
 (* Rollback. *)
 
+let freeze = get_state
+let unfreeze = set_state
+
 let with_heavy_rollback f x =
   let sum = freeze_summaries ()
   and flib = freeze() in
diff --git a/library/states.mli b/library/states.mli
index 4ac371227..46cc2f68d 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -9,6 +9,10 @@
 val intern_state : string -> unit
 val extern_state : string -> unit
 
+type state
+val freeze : unit -> state
+val unfreeze : state -> unit
+
 (*s Rollback. [with_heavy_rollback f x] applies [f] to [x] and restores the
   state of the whole system as it was before the evaluation if an exception 
   is raised. *)