Rename Ephemeron -> CEphemeron.

Fixes compilation of Coq with OCaml 4.03 beta 1.

18 files changed, 46 insertions, 46 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index 0d36e3a0f..902ab9ddf 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -32,7 +32,7 @@ CStack
 Util
 Ppstyle
 Errors
-Ephemeron
+CEphemeron
 Future
 CUnix
 System
diff --git a/dev/printers.mllib b/dev/printers.mllib
index ab7e9fc34..ad9a5d75e 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -48,7 +48,7 @@ Rtree
 Heap
 Genarg
 Stateid
-Ephemeron
+CEphemeron
 Future
 RemoteCounter
 Monad
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index fc7e1b937..7e1a5d5b7 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -131,8 +131,8 @@ let key rk =
   match !rk with
   | None -> raise NotEvaluated
   | Some k ->
-      try Ephemeron.get k
-      with Ephemeron.InvalidKey -> raise NotEvaluated
+      try CEphemeron.get k
+      with CEphemeron.InvalidKey -> raise NotEvaluated
 
 (************************)
 (* traduction des patch *)
@@ -171,7 +171,7 @@ let rec slot_for_getglobal env kn =
 	 | BCconstant -> set_global (val_of_constant kn)
     in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
-    rk := Some (Ephemeron.create pos);
+    rk := Some (CEphemeron.create pos);
     pos
 
 and slot_for_fv env fv =
diff --git a/kernel/entries.mli b/kernel/entries.mli
index b2a77dd95..f94068f31 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -104,7 +104,7 @@ type side_eff =
   | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
 
 type side_effect = {
-  from_env : Declarations.structure_body Ephemeron.key;
+  from_env : Declarations.structure_body CEphemeron.key;
   eff      : side_eff;
 }
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index e1fe02595..df3495569 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -25,7 +25,7 @@ open Declarations
 (* The key attached to each constant is used by the VM to retrieve previous *)
 (* evaluations of the constant. It is essentially an index in the symbols table *)
 (* used by the VM. *)
-type key = int Ephemeron.key option ref 
+type key = int CEphemeron.key option ref 
 
 (** Linking information for the native compiler. *)
 
@@ -50,17 +50,17 @@ type stratification = {
 }
 
 type val_kind =
-    | VKvalue of (values * Id.Set.t) Ephemeron.key
+    | VKvalue of (values * Id.Set.t) CEphemeron.key
     | VKnone
 
 type lazy_val = val_kind ref
 
 let force_lazy_val vk = match !vk with
 | VKnone -> None
-| VKvalue v -> try Some (Ephemeron.get v) with Ephemeron.InvalidKey -> None
+| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None
 
 let dummy_lazy_val () = ref VKnone
-let build_lazy_val vk key = vk := VKvalue (Ephemeron.create key)
+let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
 
 type named_vals = (Id.t * lazy_val) list
 
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 23f9a3f41..99d3e2e25 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -19,7 +19,7 @@ type link_info =
   | LinkedInteractive of string
   | NotLinked
 
-type key = int Ephemeron.key option ref 
+type key = int CEphemeron.key option ref 
 
 type constant_key = constant_body * (link_info ref * key)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4c3264861..0926d35f6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -231,11 +231,11 @@ let constant_entry_of_private_constant = function
 
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
-  { Entries.from_env = Ephemeron.create env.revstruct;
+  { Entries.from_env = CEphemeron.create env.revstruct;
     Entries.eff      = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
 
 let private_con_of_scheme ~kind env cl =
-  { Entries.from_env = Ephemeron.create env.revstruct;
+  { Entries.from_env = CEphemeron.create env.revstruct;
     Entries.eff      = Entries.SEscheme(
       List.map (fun (i,c) ->
         let cbo = Environ.lookup_constant c env.env in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 510f43542..fdbd1e3b1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -126,14 +126,14 @@ let check_signatures curmb sl =
     | None -> None, None
     | Some curmb ->
         try
-          let mb = Ephemeron.get mb in
+          let mb = CEphemeron.get mb in
           match sl with
           | None -> sl, None
           | Some n ->
               if List.length mb >= how_many && CList.skipn how_many mb == curmb
               then Some (n + how_many), Some mb
               else None, None
-        with Ephemeron.InvalidKey -> None, None in
+        with CEphemeron.InvalidKey -> None, None in
   let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
   sl
 
diff --git a/lib/ephemeron.ml b/lib/cEphemeron.ml
index a38ea11e1..a38ea11e1 100644
--- a/lib/ephemeron.ml
+++ b/lib/cEphemeron.ml
diff --git a/lib/ephemeron.mli b/lib/cEphemeron.mli
index 1200e4e20..1200e4e20 100644
--- a/lib/ephemeron.mli
+++ b/lib/cEphemeron.mli
diff --git a/lib/future.ml b/lib/future.ml
index 5cd2beba9..e8f33db5e 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -62,7 +62,7 @@ and 'a comp =
   | Exn of Exninfo.iexn  (* Invariant: this exception is always "fixed" as in fix_exn *)
 
 and 'a comput =
-  | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key
+  | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) CEphemeron.key
   | Finished of 'a
 
 and 'a computation = 'a comput ref
@@ -70,13 +70,13 @@ and 'a computation = 'a comput ref
 let unnamed = "unnamed"
 
 let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
-  ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x)))
+  ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x)))
 let get x =
   match !x with
   | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None))
   | Ongoing (name, x) ->
-      try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c
-      with Ephemeron.InvalidKey ->
+      try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c
+      with CEphemeron.InvalidKey ->
         name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null))
 
 type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn  ]
diff --git a/lib/lib.mllib b/lib/lib.mllib
index f3f6ad8fc..6805ce491 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -15,6 +15,6 @@ Rtree
 Heap
 Unionfind
 Genarg
-Ephemeron
+CEphemeron
 Future
 RemoteCounter
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index c47602bda..18200307a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -291,7 +291,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
     (* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
     (* 	end; *)
-    get_proof_clean true, Ephemeron.create hook
+    get_proof_clean true, CEphemeron.create hook
   end
 
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index aa47e2619..2449678a1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -163,7 +163,7 @@ let save with_clean id const (locality,_,kind) hook =
 	(locality, ConstRef kn)
   in
   if with_clean then  Pfedit.delete_current_proof ();
-  Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
+  CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
   definition_message id
 
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 23f1da1ba..e5c756f56 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,7 @@ val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
 val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
-  unit Lemmas.declaration_hook Ephemeron.key -> unit
+  unit Lemmas.declaration_hook CEphemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
    abort the proof
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f22cdbcc8..541f299d4 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,7 +36,7 @@ let find_proof_mode n =
     Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
 
 let register_proof_mode ({name = n} as m) =
-  Hashtbl.add proof_modes n (Ephemeron.create m)
+  Hashtbl.add proof_modes n (CEphemeron.create m)
 
 (* initial mode: standard mode *)
 let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
@@ -52,7 +52,7 @@ let _ =
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
     optread = begin fun () ->
-      (Ephemeron.default !default_proof_mode standard).name
+      (CEphemeron.default !default_proof_mode standard).name
     end;
     optwrite = begin fun n ->
       default_proof_mode := find_proof_mode n
@@ -83,12 +83,12 @@ type closed_proof = proof_object * proof_terminator
 
 type pstate = {
   pid : Id.t;
-  terminator : proof_terminator Ephemeron.key;
+  terminator : proof_terminator CEphemeron.key;
   endline_tactic : Tacexpr.raw_tactic_expr option;
   section_vars : Context.section_context option;
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
-  mode : proof_mode Ephemeron.key;
+  mode : proof_mode CEphemeron.key;
   universe_binders: universe_binders option;
 }
 
@@ -103,11 +103,11 @@ let current_proof_mode = ref !default_proof_mode
 let update_proof_mode () =
   match !pstates with
   | { mode = m } :: _ ->
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := m;
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ())
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ())
   | _ ->
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := find_proof_mode "No"
 
 (* combinators for the current_proof lists *)
@@ -215,9 +215,9 @@ let set_proof_mode mn =
   set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
 
 let activate_proof_mode mode =
-  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
+  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
 let disactivate_proof_mode mode =
-  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
+  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
 
 (** [start_proof sigma id str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
@@ -230,7 +230,7 @@ let disactivate_proof_mode mode =
 let start_proof sigma id ?pl str goals terminator =
   let initial_state = {
     pid = id;
-    terminator = Ephemeron.create terminator;
+    terminator = CEphemeron.create terminator;
     proof = Proof.start sigma goals;
     endline_tactic = None;
     section_vars = None;
@@ -242,7 +242,7 @@ let start_proof sigma id ?pl str goals terminator =
 let start_dependent_proof id ?pl str goals terminator =
   let initial_state = {
     pid = id;
-    terminator = Ephemeron.create terminator;
+    terminator = CEphemeron.create terminator;
     proof = Proof.dependent_start goals;
     endline_tactic = None;
     section_vars = None;
@@ -375,7 +375,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   in
   { id = pid; entries = entries; persistence = strength;
     universes = (universes, binders) },
-  fun pr_ending -> Ephemeron.get terminator pr_ending
+  fun pr_ending -> CEphemeron.get terminator pr_ending
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
@@ -423,11 +423,11 @@ let close_proof ~keep_body_ucst_separate fix_exn =
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator
+let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator
 let set_terminator hook =
   match !pstates with
   | [] -> raise NoCurrentProof
-  | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps
+  | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
 
 
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index cc9732604..5f018ec39 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -314,7 +314,7 @@ module Make(T : Task) = struct
         let response = slave_respond request in
         report_status "Idle";
         marshal_response (Option.get !slave_oc) response;
-        Ephemeron.clear ()
+        CEphemeron.clear ()
       with
       | MarshalError s ->
         pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 7e0d30a63..615257a1c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -324,11 +324,11 @@ type program_info_aux = {
   prg_sign: named_context_val;
 }
 
-type program_info = program_info_aux Ephemeron.key
+type program_info = program_info_aux CEphemeron.key
 
 let get_info x =
-  try Ephemeron.get x
-  with Ephemeron.InvalidKey ->
+  try CEphemeron.get x
+  with CEphemeron.InvalidKey ->
     Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
 
 let assumption_message = Declare.assumption_message
@@ -461,7 +461,7 @@ let subst_deps_obl obls obl =
 
 module ProgMap = Map.Make(Id)
 
-let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m)
+let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
@@ -682,7 +682,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 let map_cardinal m =
   let i = ref 0 in
   ProgMap.iter (fun _ v ->
-		if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m;
+		if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
   !i
 
 exception Found of program_info
@@ -690,7 +690,7 @@ exception Found of program_info
 let map_first m =
   try
     ProgMap.iter (fun _ v ->
-		  if snd (Ephemeron.get v).prg_obligations > 0 then
+		  if snd (CEphemeron.get v).prg_obligations > 0 then
 		    raise (Found v)) m;
     assert(false)
   with Found x -> x
@@ -1016,7 +1016,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
   else (
     let len = Array.length obls in
     let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
-      progmap_add n (Ephemeron.create prg);
+      progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
@@ -1030,7 +1030,7 @@ let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(r
     (fun  (n, b, t, imps, obls) ->
      let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
-     in progmap_add n (Ephemeron.create prg)) l;
+     in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
 	if finished then finished