3 files changed, 13 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index 574be9844a..cd0b52ecaa 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -312,7 +312,10 @@ let union_evar_universe_context ctx ctx' =
     let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
     let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
 			       (Univ.ContextSet.levels ctx.uctx_local) in
-    let declarenew g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g in	
+    let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
+    let declarenew g =
+      Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
+    in
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
 	uctx_local = local;
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index c88de133d4..47a5510b0f 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -95,7 +95,11 @@ struct
   let print_char = fun c -> (); fun () -> print_char c
 
   (** {!Pp.pp}. The buffer is also flushed. *)
-  let print = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
+  let print_debug = fun s -> (); fun () -> try Pp.msg_info s; Pp.pp_flush () with e ->
+    let (e, info) = Errors.push e in raise ~info e ()
+
+  (** {!Pp.pp}. The buffer is also flushed. *)
+  let print = fun s -> (); fun () -> try Pp.msg_notice s; Pp.pp_flush () with e ->
     let (e, info) = Errors.push e in raise ~info e ()
 
   let timeout = fun n t -> (); fun () ->
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 1869f32633..35dd311a8c 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -58,6 +58,10 @@ module NonLogical : sig
   (** {!Pp.pp}. The buffer is also flushed. *)
   val print : Pp.std_ppcmds -> unit t
 
+  (* FIXME: shouldn't we have a logger instead? *)
+  (** {!Pp.pp}. The buffer is also flushed. *)
+  val print_debug : Pp.std_ppcmds -> unit t
+
   (** [Pervasives.raise]. Except that exceptions are wrapped with
       {!Exception}. *)
   val raise : ?info:Exninfo.info -> exn -> 'a t