29 files changed, 780 insertions, 188 deletions

diff --git a/CHANGES b/CHANGES
index b6793e426..917219596 100644
--- a/CHANGES
+++ b/CHANGES
@@ -4,6 +4,7 @@ Changes from V8.5beta2 to ...
 Vernacular commands
 
 - New command "Redirect" to redirect the output of a command to a file.
+- New command "Undelimit Scope" to remove the delimiter of a scope.
 
 Tactics
 
diff --git a/Makefile.build b/Makefile.build
index 9f087cb55..c7b0c5262 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -101,7 +101,7 @@ BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS)
 OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
 DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils
 
-ifeq ($(shell which codesign > /dev/null && echo $(ARCH)),Darwin)
+ifeq ($(shell which codesign 2>&1 > /dev/null && echo $(ARCH)),Darwin)
 LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist"
 CODESIGN:=codesign -s -
 else
@@ -652,7 +652,7 @@ $(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ)
 
 # votour: a small vo explorer (based on the checker)
 
-bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml
+bin/votour: lib/cObj$(BESTOBJ) checker/analyze$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml
 	$(SHOW)'OCAMLBEST -o $@'
 	$(HIDE)$(call bestocaml, -I checker,)
 
@@ -688,13 +688,13 @@ ifeq ($(LOCAL),true)
 install:
 	@echo "Nothing to install in a local build!"
 else
-install: install-coq install-coqide install-doc-$(WITHDOC)
+install: install-coq install-coqide install-doc-$(WITHDOC) install-dev
 endif
 
 install-doc-all: install-doc
 install-doc-no:
 
-.PHONY: install install-doc-all install-doc-no
+.PHONY: install install-doc-all install-doc-no install-dev
 
 #These variables are intended to be set by the caller to make
 #COQINSTALLPREFIX=
@@ -748,6 +748,10 @@ install-tools:
 	$(INSTALLLIB) tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty $(FULLCOQLIB)/tools/coqdoc
 	$(INSTALLBIN) $(TOOLS) $(FULLBINDIR)
 
+install-dev: $(DEVFILES) $(DEVPRINTERS)
+	$(foreach devf, $(DEVFILES), sed -i -e /\".\"/\"$(FULLCOQLIB)\"/g $(devf))
+	$(INSTALLLIB) $(DEVFILES) $(DEVPRINTERS) $(FULLCOQLIB)/dev
+
 # The list of .cmi to install, including the ones obtained
 # from .mli without .ml, and the ones obtained from .ml without .mli
 
diff --git a/Makefile.common b/Makefile.common
index 15ac13ff1..342ce7727 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -253,6 +253,10 @@ CSDPCERTCMO:=$(addprefix plugins/micromega/, \
   mutils.cmo 	micromega.cmo \
   sos_types.cmo sos_lib.cmo sos.cmo 	csdpcert.cmo )
 
+DEVPRINTERS:=dev/vm_printers.ml dev/top_printers.ml
+
+DEVFILES:=dev/base_include dev/include
+
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
 
 COQDEPCMO:=$(COQENVCMO) lib/system.cmo tools/coqdep_lexer.cmo tools/coqdep_common.cmo tools/coqdep.cmo
diff --git a/checker/analyze.ml b/checker/analyze.ml
new file mode 100644
index 000000000..c48b83011
--- /dev/null
+++ b/checker/analyze.ml
@@ -0,0 +1,350 @@
+(** Headers *)
+
+let prefix_small_block =         0x80
+let prefix_small_int =           0x40
+let prefix_small_string =        0x20
+
+let code_int8 =                  0x00
+let code_int16 =                 0x01
+let code_int32 =                 0x02
+let code_int64 =                 0x03
+let code_shared8 =               0x04
+let code_shared16 =              0x05
+let code_shared32 =              0x06
+let code_double_array32_little = 0x07
+let code_block32 =               0x08
+let code_string8 =               0x09
+let code_string32 =              0x0A
+let code_double_big =            0x0B
+let code_double_little =         0x0C
+let code_double_array8_big =     0x0D
+let code_double_array8_little =  0x0E
+let code_double_array32_big =    0x0F
+let code_codepointer =           0x10
+let code_infixpointer =          0x11
+let code_custom =                0x12
+let code_block64 =               0x13
+
+type code_descr =
+| CODE_INT8
+| CODE_INT16
+| CODE_INT32
+| CODE_INT64
+| CODE_SHARED8
+| CODE_SHARED16
+| CODE_SHARED32
+| CODE_DOUBLE_ARRAY32_LITTLE
+| CODE_BLOCK32
+| CODE_STRING8
+| CODE_STRING32
+| CODE_DOUBLE_BIG
+| CODE_DOUBLE_LITTLE
+| CODE_DOUBLE_ARRAY8_BIG
+| CODE_DOUBLE_ARRAY8_LITTLE
+| CODE_DOUBLE_ARRAY32_BIG
+| CODE_CODEPOINTER
+| CODE_INFIXPOINTER
+| CODE_CUSTOM
+| CODE_BLOCK64
+
+let code_max = 0x13
+
+let magic_number = "\132\149\166\190"
+
+(** Memory reification *)
+
+type repr =
+| RInt of int
+| RBlock of (int * int) (* tag × len *)
+| RString of string
+| RPointer of int
+| RCode of int
+
+type data =
+| Int of int (* value *)
+| Ptr of int (* pointer *)
+| Atm of int (* tag *)
+| Fun of int (* address *)
+
+type obj =
+| Struct of int * data array (* tag × data *)
+| String of string
+
+module type Input =
+sig
+  type t
+  val input_byte : t -> int
+  val input_binary_int : t -> int
+end
+
+module type S =
+sig
+  type input
+  val parse : input -> (data * obj array)
+end
+
+module Make(M : Input) =
+struct
+
+open M
+
+type input = M.t
+
+let current_offset = ref 0
+
+let input_byte chan =
+  let () = incr current_offset in
+  input_byte chan
+
+let input_binary_int chan =
+  let () = current_offset := !current_offset + 4 in
+  input_binary_int chan
+
+let input_char chan = Char.chr (input_byte chan)
+
+let parse_header chan =
+  let () = current_offset := 0 in
+  let magic = String.create 4 in
+  let () = for i = 0 to 3 do magic.[i] <- input_char chan done in
+  let length = input_binary_int chan in
+  let objects = input_binary_int chan in
+  let size32 = input_binary_int chan in
+  let size64 = input_binary_int chan in
+  (magic, length, size32, size64, objects)
+
+let input_int8s chan =
+  let i = input_byte chan in
+  if i land 0x80 = 0
+    then i
+    else i lor ((-1) lsl 8)
+
+let input_int8u = input_byte
+
+let input_int16s chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let ans = (i lsl 8) lor j in
+  if i land 0x80 = 0
+    then ans
+    else ans lor ((-1) lsl 16)
+
+let input_int16u chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  (i lsl 8) lor j
+
+let input_int32s chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in
+  if i land 0x80 = 0
+    then ans
+    else ans lor ((-1) lsl 31)
+
+let input_int32u chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l
+
+let input_int64s chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let m = input_byte chan in
+  let n = input_byte chan in
+  let o = input_byte chan in
+  let p = input_byte chan in
+  let ans =
+    (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+    (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p
+  in
+  if i land 0x80 = 0
+    then ans
+    else ans lor ((-1) lsl 63)
+
+let input_int64u chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let m = input_byte chan in
+  let n = input_byte chan in
+  let o = input_byte chan in
+  let p = input_byte chan in
+  (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
+  (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p
+
+let input_header32 chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let tag = l in
+  let len = (i lsl 14) lor (j lsl 6) lor (k lsr 2) in
+  (tag, len)
+
+let input_header64 chan =
+  let i = input_byte chan in
+  let j = input_byte chan in
+  let k = input_byte chan in
+  let l = input_byte chan in
+  let m = input_byte chan in
+  let n = input_byte chan in
+  let o = input_byte chan in
+  let p = input_byte chan in
+  let tag = p in
+  let len =
+    (i lsl 46) lor (j lsl 38) lor (k lsl 30) lor (l lsl 22) lor
+    (m lsl 14) lor (n lsl 6) lor (o lsr 2)
+  in
+  (tag, len)
+
+let input_string len chan =
+  let ans = String.create len in
+  for i = 0 to pred len do
+    ans.[i] <- input_char chan;
+  done;
+  ans
+
+let parse_object chan =
+  let data = input_byte chan in
+  if prefix_small_block <= data then
+    let tag = data land 0x0F in
+    let len = (data lsr 4) land 0x07 in
+    RBlock (tag, len)
+  else if prefix_small_int <= data then
+    RInt (data land 0x3F)
+  else if prefix_small_string <= data then
+    let len = data land 0x1F in
+    RString (input_string len chan)
+  else if data > code_max then
+    assert false
+  else match (Obj.magic data) with
+  | CODE_INT8 ->
+    RInt (input_int8s chan)
+  | CODE_INT16 ->
+    RInt (input_int16s chan)
+  | CODE_INT32 ->
+    RInt (input_int32s chan)
+  | CODE_INT64 ->
+    RInt (input_int64s chan)
+  | CODE_SHARED8 ->
+    RPointer (input_int8u chan)
+  | CODE_SHARED16 ->
+    RPointer (input_int16u chan)
+  | CODE_SHARED32 ->
+    RPointer (input_int32u chan)
+  | CODE_BLOCK32 ->
+    RBlock (input_header32 chan)
+  | CODE_BLOCK64 ->
+    RBlock (input_header64 chan)
+  | CODE_STRING8 ->
+    let len = input_int8u chan in
+    RString (input_string len chan)
+  | CODE_STRING32 ->
+    let len = input_int32u chan in
+    RString (input_string len chan)
+  | CODE_CODEPOINTER ->
+    let addr = input_int32u chan in
+    for i = 0 to 15 do ignore (input_byte chan); done;
+    RCode addr
+  | CODE_DOUBLE_ARRAY32_LITTLE
+  | CODE_DOUBLE_BIG
+  | CODE_DOUBLE_LITTLE
+  | CODE_DOUBLE_ARRAY8_BIG
+  | CODE_DOUBLE_ARRAY8_LITTLE
+  | CODE_DOUBLE_ARRAY32_BIG
+  | CODE_INFIXPOINTER
+  | CODE_CUSTOM ->
+    Printf.eprintf "Unhandled code %04x\n%!" data; assert false
+
+let parse chan =
+  let (magic, len, _, _, size) = parse_header chan in
+  let () = assert (magic = magic_number) in
+  let memory = Array.make size (Struct ((-1), [||])) in
+  let current_object = ref 0 in
+  let fill_obj = function
+  | RPointer n ->
+    let data = Ptr (!current_object - n) in
+    data, None
+  | RInt n ->
+    let data = Int n in
+    data, None
+  | RString s ->
+    let data = Ptr !current_object in
+    let () = memory.(!current_object) <- String s in
+    let () = incr current_object in
+    data, None
+  | RBlock (tag, 0) ->
+    (* Atoms are never shared *)
+    let data = Atm tag in
+    data, None
+  | RBlock (tag, len) ->
+    let data = Ptr !current_object in
+    let nblock = Array.make len (Atm (-1)) in
+    let () = memory.(!current_object) <- Struct (tag, nblock) in
+    let () = incr current_object in
+    data, Some nblock
+  | RCode addr ->
+    let data = Fun addr in
+    data, None
+  in
+
+  let rec fill block off accu =
+    if Array.length block = off then
+      match accu with
+      | [] -> ()
+      | (block, off) :: accu -> fill block off accu
+    else
+      let data, nobj = fill_obj (parse_object chan) in
+      let () = block.(off) <- data in
+      let block, off, accu = match nobj with
+      | None -> block, succ off, accu
+      | Some nblock -> nblock, 0, ((block, succ off) :: accu)
+      in
+      fill block off accu
+  in
+  let ans = [|Atm (-1)|] in
+  let () = fill ans 0 [] in
+  (ans.(0), memory)
+
+end
+
+module IChannel =
+struct
+  type t = in_channel
+  let input_byte = Pervasives.input_byte
+  let input_binary_int = Pervasives.input_binary_int
+end
+
+module IString =
+struct
+  type t = (string * int ref)
+
+  let input_byte (s, off) =
+    let ans = Char.code (s.[!off]) in
+    let () = incr off in
+    ans
+
+  let input_binary_int chan =
+    let i = input_byte chan in
+    let j = input_byte chan in
+    let k = input_byte chan in
+    let l = input_byte chan in
+    let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in
+    if i land 0x80 = 0
+      then ans
+      else ans lor ((-1) lsl 31)
+
+end
+
+module PChannel = Make(IChannel)
+module PString = Make(IString)
+
+let parse_channel = PChannel.parse
+let parse_string s = PString.parse (s, ref 0)
diff --git a/checker/analyze.mli b/checker/analyze.mli
new file mode 100644
index 000000000..42efcf01d
--- /dev/null
+++ b/checker/analyze.mli
@@ -0,0 +1,35 @@
+type data =
+| Int of int
+| Ptr of int
+| Atm of int (* tag *)
+| Fun of int (* address *)
+
+type obj =
+| Struct of int * data array (* tag × data *)
+| String of string
+
+val parse_channel : in_channel -> (data * obj array)
+val parse_string : string -> (data * obj array)
+
+(** {6 Functorized version} *)
+
+module type Input =
+sig
+  type t
+  val input_byte : t -> int
+  (** Input a single byte *)
+  val input_binary_int : t -> int
+  (** Input a big-endian 31-bits signed integer *)
+end
+(** Type of inputs *)
+
+module type S =
+sig
+  type input
+  val parse : input -> (data * obj array)
+  (** Return the entry point and the reification of the memory out of a
+      marshalled structure. *)
+end
+
+module Make (M : Input) : S with type input = M.t
+(** Functorized version of the previous code. *)
diff --git a/checker/votour.ml b/checker/votour.ml
index bb8e06702..4aecb28f2 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -21,32 +21,91 @@ sig
   type obj
   val input : in_channel -> obj
   val repr : obj -> obj repr
-  val size : int list -> int
+  val size : obj -> int
 end
 
-module Repr : S =
+module ReprObj : S =
 struct
-  type obj = Obj.t
+  type obj = Obj.t * int list
 
   let input chan =
     let obj = input_value chan in
     let () = CObj.register_shared_size obj in
-    obj
+    (obj, [])
 
-  let repr obj =
+  let repr (obj, pos) =
     if Obj.is_block obj then
       let tag = Obj.tag obj in
       if tag = Obj.string_tag then STRING (Obj.magic obj)
       else if tag < Obj.no_scan_tag then
-        let data = Obj.dup obj in
-        let () = Obj.set_tag data 0 in
+        let init i = (Obj.field obj i, i :: pos) in
+        let data = Array.init (Obj.size obj) init in
         BLOCK (tag, Obj.magic data)
       else OTHER
     else INT (Obj.magic obj)
 
-  let size p = CObj.shared_size_of_pos p
+  let size (_, p) = CObj.shared_size_of_pos p
 end
 
+module ReprMem : S =
+struct
+  open Analyze
+
+  type obj = data
+
+  let memory = ref [||]
+  let sizes = ref [||]
+  (** size, in words *)
+
+  let ws = Sys.word_size / 8
+
+  let rec init_size seen = function
+  | Int _ | Atm _ | Fun _ -> 0
+  | Ptr p ->
+    if seen.(p) then 0
+    else
+      let () = seen.(p) <- true in
+      match (!memory).(p) with
+      | Struct (tag, os) ->
+        let fold accu o = accu + 1 + init_size seen o in
+        let size = Array.fold_left fold 1 os in
+        let () = (!sizes).(p) <- size in
+        size
+      | String s ->
+        let size = 2 + (String.length s / ws) in
+        let () = (!sizes).(p) <- size in
+        size
+
+  let size = function
+  | Int _ | Atm _ | Fun _ -> 0
+  | Ptr p -> (!sizes).(p)
+
+  let repr = function
+  | Int i -> INT i
+  | Atm t -> BLOCK (t, [||])
+  | Fun _ -> OTHER
+  | Ptr p ->
+    match (!memory).(p) with
+    | Struct (tag, os) -> BLOCK (tag, os)
+    | String s -> STRING s
+
+  let input ch =
+    let obj, mem = parse_channel ch in
+    let () = memory := mem in
+    let () = sizes := Array.make (Array.length mem) (-1) in
+    let seen = Array.make (Array.length mem) false in
+    let _ = init_size seen obj in
+    obj
+
+end
+
+module Visit (Repr : S) :
+sig
+  val init : unit -> unit
+  val visit : Values.value -> Repr.obj -> int list -> unit
+end =
+struct
+
 (** Name of a value *)
 
 let rec get_name ?(extra=false) = function
@@ -92,7 +151,7 @@ let rec get_details v o = match v, Repr.repr o with
 
 let node_info (v,o,p) =
   get_name ~extra:true v ^ get_details v o ^
-    " (size "^ string_of_int (Repr.size p)^"w)"
+    " (size "^ string_of_int (Repr.size o)^"w)"
 
 (** Children of a block : type, object, position.
     For lists, we collect all elements of the list at once *)
@@ -201,6 +260,8 @@ let rec visit v o pos =
   | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos
   | Failure _ | Invalid_argument _ -> visit v o pos
 
+end
+
 (** Loading the vo *)
 
 type header = {
@@ -256,6 +317,12 @@ let visit_vo f =
     make_seg "STM tasks" (Opt Values.v_stm_seg);
     make_seg "opaque proofs" Values.v_opaques;
   |] in
+  let repr =
+    if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S)
+    (** On 32-bit machines, representation may exceed the max size of arrays *)
+  in
+  let module Repr = (val repr : S) in
+  let module Visit = Visit(Repr) in
   while true do
     let ch = open_in_bin f in
     let magic = input_binary_int ch in
@@ -279,8 +346,8 @@ let visit_vo f =
     let seg = int_of_string l in
     seek_in ch segments.(seg).pos;
     let o = Repr.input ch in
-    let () = init () in
-    visit segments.(seg).typ o []
+    let () = Visit.init () in
+    Visit.visit segments.(seg).typ o []
   done
 
 let main =
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 37cbd1eac..aabc8a899 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -757,7 +757,8 @@ ways to change the interpretation of subterms are available.
 \subsubsection{Local opening of an interpretation scope 
 \label{scopechange}
 \index{\%}
-\comindex{Delimit Scope}}
+\comindex{Delimit Scope}
+\comindex{Undelimit Scope}}
 
 It is possible to locally extend the interpretation scope stack using
 the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey}
@@ -774,6 +775,12 @@ To bind a delimiting key to a scope, use the command
 \texttt{Delimit Scope} {\scope} \texttt{with} {\ident} 
 \end{quote}
 
+To remove a delimiting key of a scope, use the command
+
+\begin{quote}
+\texttt{Undelimit Scope} {\scope}
+\end{quote}
+
 \subsubsection{Binding arguments of a constant to an interpretation scope
 \comindex{Arguments}}
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 94290bc80..072939106 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -11,7 +11,7 @@ with {\ocaml} code statically linked, with the tool {\tt
   coqmktop}.
 
 For example, one can build a native-code \Coq\ toplevel extended with a tactic
-which source is in {\tt tactic.ml} with the command 
+which source is in {\tt tactic.ml} with the command
 \begin{verbatim}
      % coqmktop -opt -o mytop.out tactic.cmx
 \end{verbatim}
@@ -49,7 +49,7 @@ which detects the executables containing the word \texttt{coq}. In
 this case, the debugger is called with the required additional
 arguments. In other cases, the debugger is simply called without additional
 arguments. Such a wrapper can be found in the \texttt{dev/}
-subdirectory of the sources. 
+subdirectory of the sources.
 
 \section[Modules dependencies]{Modules dependencies\label{Dependencies}\index{Dependencies}
   \ttindex{coqdep}}
@@ -74,76 +74,109 @@ instead for the \ocaml\ modules dependencies.
 See the man page of {\tt coqdep} for more details and options.
 
 
-\section[Creating a {\tt Makefile} for \Coq\ modules]{Creating a {\tt Makefile} for \Coq\ modules\label{Makefile}
+\section[Creating a {\tt Makefile} for \Coq\ modules]
+{Creating a {\tt Makefile} for \Coq\ modules
+\label{Makefile}
 \ttindex{Makefile}
-\ttindex{coq\_Makefile}}
-
-\paragraph{\_CoqProject}
-When a proof development becomes a larger project, split into several
-files or containing {\ocaml} plugins, files share common options that
-must be specified to all the executables used during the development
-of the project. It is therefore convenient to write a file that could
-be read all the components (the IDE, the compiler, etc.) that
-specify all the files and the common options of the project.
-
-An attempt to set up a format to write project files has been made
-from the command line option of the {\Coq} makefile generator
-\texttt{coq\_makefile}. It is described by \texttt{\% coq\_makefile
-  --help}. The default name for the project file understood by
-\texttt{coq\_makefile}, \texttt{coqide} and \texttt{Proof General} is
-\texttt{\_CoqProject}.
-
-A minimal usable project file can probably be obtained by the
-invocation
+\ttindex{coq\_Makefile}
+\ttindex{\_CoqProject}}
+
+A project is a proof development split into several files, possibly
+including the sources of some {\ocaml} plugins, that are located (in
+various sub-directories of) a certain directory. The
+\texttt{coq\_makefile} command allows to generate generic and complete
+\texttt{Makefile} files, that can be used to compile the different
+components of the project. A \_CoqProject file
+specifies both the list of target files relevant to the project
+and the common options that should be passed to each executable at
+compilation times, for the IDE, etc.
+
+\paragraph{\_CoqProject file as an argument to  coq\_Makefile.}
+In particular, a \_CoqProject file contains the relevant
+arguments to be passed to the \texttt{coq\_makefile} makefile
+generator using for instance the command:
+
+\begin{quotation}
+\texttt{\% coq\_makefile -f \_CoqProject -o Makefile}
+\end{quotation}
+
+This command generates a file \texttt{Makefile} that can be used to
+compile all the sources of the current project. It follows the
+syntax described by the output of \texttt{\% coq\_makefile --help}.
+Once the \texttt{Makefile} file has been generated a first time, it
+can be used by the \texttt{make} command to compile part or all of
+the project. Note that once it has been generated once, as soon as
+\texttt{\_CoqProject} file is updated, the \texttt{Makefile} file is
+automatically regenerated by an invocation of \texttt{make}.
+
+The following command generates a minimal example of
+\texttt{\_CoqProject} file:
 \begin{quotation}
 \texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name
   '*.v' -print \} > \_CoqProject}
 \end{quotation}
+when executed at the root of the directory containing the
+project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files
+that are present in the current directory and its sub-directories. But no
+plugin sources is listed. If a \texttt{Makefile} is generated from
+this \texttt{\_CoqProject}, the command \texttt{make install} will
+install the compiled project in a sub-directory \texttt{MyFancyLib} of
+the \texttt{user-contrib} directory  (of the user's {\Coq} libraries
+location). This sub-directory is created if it does not already exist.
+
+\paragraph{\_CoqProject file as a configuration for IDEs.}
+
+A \texttt{\_CoqProject} file can also be used to configure the options
+of the \texttt{coqtop} process executed by a user interface. This
+allows to import the libraries of the project under a correct name,
+both as a developer of the project, working in the directory
+containing its sources, and as a user, using the project after
+the installation of its libraries. Currently, both \CoqIDE{} and Proof
+General (version $\geq$ 4.3pre) support configuration via
+\texttt{\_CoqProject} files.
+
+\paragraph{Remarks.}
 
-While customizing a project file, mind the following requirements:
 \begin{itemize}
-\item {\Coq} files must end in \texttt{.v}, {\ocaml} modules in
-  \texttt{.ml4} if they require camlp preprocessing (and in
-  \texttt{.ml} otherwise), {\ocaml} module signatures, library
-  description and packing files respectively in \texttt{.mli},
-  \texttt{.mllib} and \texttt{.mlpack}.
-
-Any other argument that is not a valid option will be considered as a
-subdirectory. A specified subdirectory must have an inner
-\texttt{Makefile}. The phony targets \texttt{all} and \texttt{clean}
-will recursively call this target in all the subdirectories.
-
-\item \texttt{-R} and \texttt{-Q} options are for {\Coq}, \texttt{-I}
-  for {\ocaml}. The same directory may be ``included'' by both.
-
-  Using \texttt{-R} or \texttt{-Q} gives a correct logical path
-  and a correct installation location to your coq files.
-\item dependency on an external library must not be declared using a
-  \texttt{-Q \dots} in the \texttt{\_CoqProject} to include it in the
-  path, as the \textit{make clean} command would erase it! Instead,
-  install your dependency in a place automatically included by
-  {\Coq}. You can take advantage of the \texttt{COQPATH} variable
-  (see \ref{envars}) without installation if necessary.
-\item Use \texttt{-extra-phony} with no command to add an extra
+\item Every {\Coq} files must use a \texttt{.v} file extension.
+ The {\ocaml} modules must use a \texttt{.ml4} file extension
+ if they require camlp preprocessing (and in \texttt{.ml} otherwise).
+ The {\ocaml} module signatures, library
+ description and packing files must use respectively \texttt{.mli},
+ \texttt{.mllib} and \texttt{.mlpack} file extension.
+
+\item Any argument that is not a valid option is considered as a
+  sub-directory. Any sub-directory specified in the list of targets must
+  itself contain a \texttt{Makefile}.
+
+\item The phony targets \texttt{all} and \texttt{clean} recursively
+  call their target in every sub-directory.
+
+\item \texttt{-R} and \texttt{-Q} options are for {\Coq} files, \texttt{-I}
+  for {\ocaml} ones. A same directory can be passed to both nature of
+  options, in the same \texttt{\_CoqProject}.
+
+\item Using \texttt{-R} or \texttt{-Q} is the appropriate way to
+  obtain both a correct logical path and a correct installation location to
+  the libraries of a given project.
+
+\item Dependencies on external libraries to the project must be
+  declared with care. If in the \texttt{\_CoqProject} file an external
+  library \texttt{foo} is passed to a \texttt{-Q} option, like in
+  \texttt{-Q foo}, the subsequent \textit{make clean} command can
+  erase \textit{foo}. It is hence safer to customize the
+  \texttt{COQPATH} variable (see \ref{envars}), to include the
+  location of the required external libraries.
+
+\item Using \texttt{-extra-phony} with no command adds extra
   dependencies on already defined rules. For example the following
-  skeleton appends something to the \texttt{install} rule:
+  skeleton appends ``something'' to the \texttt{install} rule:
 \begin{quotation}
 \texttt{-extra-phony "install" "install-my-stuff" ""
   -extra-phony "install-my-stuff" "" "something"}
 \end{quotation}
 \end{itemize}
 
-\paragraph{Coq\_makefile}
-The writing of a generic and complete \texttt{Makefile} may be tedious
-work and that's why {\Coq} provides a tool to automate its creation
-from the \texttt{\_CoqProject} file, \texttt{coq\_makefile}.
-
-Use
-\begin{quotation}
-\texttt{coq\_makefile -f \_CoqProject -o Makefile}
-\end{quotation}
-to generate a \texttt{Makefile} the first time. \texttt{Makefile} will be
-automatically regenerated when \texttt{\_CoqProject} is updated afterward.
 
 \section[Documenting \Coq\ files with coqdoc]{Documenting \Coq\ files with coqdoc\label{coqdoc}
 \ttindex{coqdoc}}
@@ -212,10 +245,10 @@ Instructions to use it are contained in this file.
 {\ProofGeneral} is a generic interface for proof assistants based on
 Emacs. The main idea is that the \Coq\ commands you are
 editing are sent to a \Coq\ toplevel running behind Emacs and the
-answers of the system automatically inserted into other Emacs buffers. 
+answers of the system automatically inserted into other Emacs buffers.
 Thus you don't need to copy-paste the \Coq\ material from your files
 to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some
-files. 
+files.
 
 {\ProofGeneral} is developed and distributed independently of the
 system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!.
@@ -242,7 +275,7 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and
 \RefManCutCommand{ENDREFMAN=\thepage}
 %END LATEX
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: t
-%%% End: 
+%%% End:
diff --git a/engine/evd.ml b/engine/evd.ml
index 60b1da704..168a10df9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -351,10 +351,7 @@ let evar_universe_context_of ctx = { empty_evar_universe_context with uctx_local
 let evar_universe_context_subst ctx = ctx.uctx_univ_variables
 
 let instantiate_variable l b v =
-  (* let b = Univ.subst_large_constraint (Univ.Universe.make l) Univ.type0m_univ b in *)
-  (* if Univ.univ_depends (Univ.Universe.make l) b then  *)
-  (*   error ("Occur-check in universe variable instantiation") *)
-  (* else *) v := Univ.LMap.add l (Some b) !v
+  v := Univ.LMap.add l (Some b) !v
 
 exception UniversesDiffer
 
@@ -420,7 +417,16 @@ let process_universe_constraints univs vars alg cstrs =
 		      raise UniversesDiffer
 	      in
 	        Univ.enforce_eq_level l' r' local
-           | _, _ (* One of the two is algebraic or global *) -> 
+	    | Inr (l, loc, alg), Inl r
+	    | Inl r, Inr (l, loc, alg) ->
+	       let inst = Univ.univ_level_rem l r r in
+		 if alg then (instantiate_variable l inst vars; local)
+		 else
+		   let lu = Univ.Universe.make l in
+		   if Univ.univ_level_mem l r then
+		     Univ.enforce_leq inst lu local
+		   else raise (Univ.UniverseInconsistency (Univ.Eq, lu, r, None))
+            | _, _ (* One of the two is algebraic or global *) -> 
 	     if Univ.check_eq univs l r then local
 	     else raise (Univ.UniverseInconsistency (Univ.Eq, l, r, None))
   in
diff --git a/interp/notation.ml b/interp/notation.ml
index 555dfa804..0b5791d32 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -200,6 +200,19 @@ let declare_delimiters scope key =
     end
   with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
 
+let remove_delimiters scope =
+  let sc = find_scope scope in
+  let newsc = { sc with delimiters = None } in
+  match sc.delimiters with
+    | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
+    | Some key ->
+       scope_map := String.Map.add scope newsc !scope_map;
+       try
+         let _ = ignore (String.Map.find key !delimiters_map) in
+         delimiters_map := String.Map.remove key !delimiters_map
+       with Not_found ->
+         assert false (* A delimiter for scope [scope] should exist *)
+
 let find_delimiters_scope loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
diff --git a/interp/notation.mli b/interp/notation.mli
index 854c52b2c..38bd5fc7b 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -55,6 +55,7 @@ val find_scope : scope_name -> scope
 (** Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
+val remove_delimiters : scope_name -> unit
 val find_delimiters_scope : Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index d7b269a1d..0ca3bb35f 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -284,7 +284,7 @@ type vernac_expr =
   | VernacSyntaxExtension of
       obsolete_locality * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
-  | VernacDelimiters of scope_name * string
+  | VernacDelimiters of scope_name * string option
   | VernacBindScope of scope_name * reference or_by_notation list
   | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
       constr_expr * scope_name option
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index ae86d686a..e2854abfd 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -26,8 +26,8 @@ let univ_of_sort = function
   | Prop Null -> Universe.type0m
 
 let sort_of_univ u =
-  if is_type0m_univ u then Prop Null
-  else if is_type0_univ u then Prop Pos
+  if is_type0m_univ u then prop
+  else if is_type0_univ u then set
   else Type u
 
 let compare s1 s2 =
@@ -62,6 +62,8 @@ let is_small = function
 let family = function
   | Prop Null -> InProp
   | Prop Pos -> InSet
+  | Type u when is_type0m_univ u -> InProp
+  | Type u when is_type0_univ u -> InSet
   | Type _ -> InType
 
 let family_equal = (==)
@@ -76,7 +78,7 @@ let hash = function
   in
   combinesmall 1 h
 | Type u ->
-  let h = Hashtbl.hash u in (** FIXME *)
+ let h = Univ.Universe.hash u in
   combinesmall 2 h
 
 module List = struct
@@ -101,7 +103,7 @@ module Hsorts =
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
 
-      let hash = Hashtbl.hash (** FIXME *)
+      let hash = hash
     end)
 
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 4af7fe7c1..fce9e28d3 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -925,25 +925,7 @@ let fast_compare_neq strict g arcu arcv =
     if arc_is_lt arc then
       cmp c to_revert lt_todo le_todo
     else
-      let rec find lt_todo lt le = match le with
-      | [] ->
-        begin match lt with
-        | [] ->
-          let () = arc.status <- SetLt in
-          cmp c (arc :: to_revert) lt_todo le_todo
-        | u :: lt ->
-          let arc = repr g u in
-          if arc == arcv then
-            if strict then (to_revert, FastLT) else (to_revert, FastLE)
-          else find (arc :: lt_todo) lt le
-        end
-      | u :: le ->
-        let arc = repr g u in
-        if arc == arcv then
-          if strict then (to_revert, FastLT) else (to_revert, FastLE)
-        else find (arc :: lt_todo) lt le
-      in
-      find lt_todo arc.lt arc.le
+      process_lt c to_revert lt_todo le_todo arc arc.lt arc.le
   | [], arc::le_todo ->
     if arc == arcv then
       (* No need to continue inspecting universes above arc:
@@ -955,23 +937,43 @@ let fast_compare_neq strict g arcu arcv =
       if arc_is_le arc then
         cmp c to_revert [] le_todo
       else
-        let rec find lt_todo lt = match lt with
-        | [] ->
-          let fold accu u =
-            let node = repr g u in
-            node :: accu
-          in
-          let le_new = List.fold_left fold le_todo arc.le in
-          let () = arc.status <- SetLe in
-          cmp c (arc :: to_revert) lt_todo le_new
-        | u :: lt ->
-          let arc = repr g u in
-          if arc == arcv then
-            if strict then (to_revert, FastLT) else (to_revert, FastLE)
-          else find (arc :: lt_todo) lt
-        in
-        find [] arc.lt
+        process_le c to_revert [] le_todo arc arc.lt
+
+  and process_lt c to_revert lt_todo le_todo arc0 lt le = match le with
+  | [] ->
+    begin match lt with
+    | [] ->
+      let () = arc0.status <- SetLt in
+      cmp c (arc0 :: to_revert) lt_todo le_todo
+    | u :: lt ->
+      let arc = repr g u in
+      if arc == arcv then
+        if strict then (to_revert, FastLT) else (to_revert, FastLE)
+      else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le
+    end
+  | u :: le ->
+    let arc = repr g u in
+    if arc == arcv then
+      if strict then (to_revert, FastLT) else (to_revert, FastLE)
+    else process_lt c to_revert (arc :: lt_todo) le_todo arc0 lt le
+
+  and process_le c to_revert lt_todo le_todo arc0 lt = match lt with
+  | [] ->
+    let fold accu u =
+      let node = repr g u in
+      node :: accu
+    in
+    let le_new = List.fold_left fold le_todo arc0.le in
+    let () = arc0.status <- SetLe in
+    cmp c (arc0 :: to_revert) lt_todo le_new
+  | u :: lt ->
+    let arc = repr g u in
+    if arc == arcv then
+      if strict then (to_revert, FastLT) else (to_revert, FastLE)
+    else process_le c to_revert (arc :: lt_todo) le_todo arc0 lt
+
   in
+
   try
     let (to_revert, c) = cmp FastNLE [] [] [arcu] in
     (** Reset all the touched arcs. *)
diff --git a/library/universes.ml b/library/universes.ml
index 16e6ebb02..a3926bc6f 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -757,7 +757,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	if alg then
 	  (* u is algebraic: we instantiate it with it's lower bound, if any, 
               or enforce the constraints if it is bounded from the top. *)
-	  instantiate_with_lbound u lbound true (not (Option.is_empty right)) acc
+	  instantiate_with_lbound u lbound true false acc
 	else (* u is non algebraic *)
 	  match Universe.level lbound with
 	  | Some l -> (* The lowerbound is directly a level *) 
@@ -767,7 +767,8 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	     if not (Level.equal l u) then
 	       (* Should check that u does not 
   	          have upper constraints that are not already in right *)
-	       instantiate_with_lbound u lbound false (LSet.mem l algs) acc
+	       let acc' = (ctx', us, LSet.remove l algs, insts, cstrs) in
+		 instantiate_with_lbound u lbound false false acc
 	     else acc, (true, false, lbound)
 	| None -> 
 	  try 
@@ -1017,13 +1018,14 @@ let solve_constraints_system levels level_bounds level_min =
   for i=0 to nind-1 do
     for j=0 to nind-1 do
       if not (Int.equal i j) && Int.Set.mem j clos.(i) then
-	(v.(i) <- Universe.sup v.(i) level_bounds.(j);
-	 level_min.(i) <- Universe.sup level_min.(i) level_min.(j))
+	(v.(i) <- Universe.sup v.(i) level_bounds.(j));
+	 (* level_min.(i) <- Universe.sup level_min.(i) level_min.(j)) *)
     done;
-    for j=0 to nind-1 do
-      match levels.(j) with
-      | Some u -> v.(i) <- univ_level_rem u v.(i) level_min.(i)
-      | None -> ()
-    done
+    (* for j=0 to nind-1 do *)
+    (*   match levels.(j) with *)
+    (*   | Some u when not (Univ.Level.is_small u) -> *)
+    (* 	 v.(i) <- univ_level_rem u v.(i) level_min.(i) *)
+    (*   | _ -> () *)
+    (* done *)
   done;
   v
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e8a1b512c..fe9c58240 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -96,12 +96,12 @@ GEXTEND Gram
       | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
       | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
 
-      | v = vernac_poly -> v ] 
+      | v = vernac_poly -> v ]
     ]
   ;
-  vernac_poly: 
+  vernac_poly:
     [ [ IDENT "Polymorphic"; v = vernac_aux -> VernacPolymorphic (true, v)
-      | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v) 
+      | IDENT "Monomorphic"; v = vernac_aux -> VernacPolymorphic (false, v)
       | v = vernac_aux -> v ]
     ]
   ;
@@ -146,7 +146,7 @@ GEXTEND Gram
     ] ]
   ;
 
-  subgoal_command: 
+  subgoal_command:
     [ [ c = query_command; "." ->
                   begin function
                     | Some (SelectNth g) -> c (Some g)
@@ -1043,7 +1043,9 @@ GEXTEND Gram
          VernacOpenCloseScope (local,(false,sc))
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
-	 VernacDelimiters (sc,key)
+	 VernacDelimiters (sc, Some key)
+     | IDENT "Undelimit"; IDENT "Scope"; sc = IDENT ->
+	 VernacDelimiters (sc, None)
 
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
        refl = LIST1 smart_global -> VernacBindScope (sc,refl)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dd671f111..dc70f36cc 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1287,7 +1287,9 @@ let sigma_compare_sorts env pb s0 s1 sigma =
     
 let sigma_compare_instances flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
-  with Evd.UniversesDiffer -> raise Reduction.NotConvertible
+  with Evd.UniversesDiffer
+     | Univ.UniverseInconsistency _ ->
+	raise Reduction.NotConvertible
 
 let sigma_univ_state = 
   { Reduction.compare = sigma_compare_sorts;
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 832c08fe0..4e889e55f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -644,11 +644,15 @@ module Make
             keyword (if opening then "Open " else "Close ") ++
               keyword "Scope" ++ spc() ++ str sc
           )
-        | VernacDelimiters (sc,key) ->
+        | VernacDelimiters (sc,Some key) ->
           return (
             keyword "Delimit Scope" ++ spc () ++ str sc ++
               spc() ++ keyword "with" ++ spc () ++ str key
           )
+        | VernacDelimiters (sc, None) ->
+          return (
+            keyword "Undelimit Scope" ++ spc () ++ str sc
+          )
         | VernacBindScope (sc,cll) ->
           return (
             keyword "Bind Scope" ++ spc () ++ str sc ++
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 9edc1f1c7..aaa6c2c07 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -509,8 +509,10 @@ let rec tmpp v loc =
 
   | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
   | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
-  | VernacDelimiters (name,tag) ->
+  | VernacDelimiters (name,Some tag) ->
       xmlScope loc "delimit" name ~attr:["delimiter",tag] []
+  | VernacDelimiters (name,None) ->
+      xmlScope loc "undelimit" name ~attr:[] []
   | VernacBindScope (name,l) ->
       xmlScope loc "bind" name
         (List.map (function
diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v
index 4f29b76c6..dce73e1a5 100644
--- a/test-suite/bugs/closed/3446.v
+++ b/test-suite/bugs/closed/3446.v
@@ -1,28 +1,32 @@
 (* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *)
-(* Set Asymmetric Patterns. *)
-(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *)
-(* Notation "A -> B" := (forall (_ : A), B). *)
+Module First.
+Set Asymmetric Patterns.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B).
+Set Universe Polymorphism.
+
 
-(* Notation "x → y" := (x -> y) *)
-(*   (at level 99, y at level 200, right associativity): type_scope. *)
-(* Record sigT A (P : A -> Type) := *)
-(*   { projT1 : A ; projT2 : P projT1 }. *)
-(* Arguments projT1 {A P} s. *)
-(* Arguments projT2 {A P} s. *)
-(* Set Universe Polymorphism. *)
-(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *)
-(* Reserved Notation "x = y" (at level 70, no associativity). *)
-(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *)
-(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *)
-(* Reserved Notation "{ x : A  & P }" (at level 0, x at level 99). *)
-(* Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope. *)
+Notation "x → y" := (x -> y)
+  (at level 99, y at level 200, right associativity): type_scope.
+Record sigT A (P : A -> Type) :=
+  { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} s.
+Arguments projT2 {A P} s.
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Reserved Notation "x = y" (at level 70, no associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y).
+Notation " x = y " := (paths x y) : type_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
+Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope.
 
 
-(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v. *)
-(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *)
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v.
+Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}).
 
-(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *)
-(*   @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *)
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) :=
+  @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _).
+End First.
 
 Set Asymmetric Patterns.
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 932084891..0ccc92067 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -43,7 +43,7 @@ Notation IsHProp := (IsTrunc -1).
 Monomorphic Axiom dummy_funext_type : Type0.
 Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
 
-Inductive Unit : Type1 :=
+Inductive Unit : Set :=
     tt : Unit.
 
 Record TruncType (n : trunc_index) := BuildTruncType {
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index 1449f242b..c6cb9c35e 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -163,7 +163,7 @@ Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
 
 Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
 
-Inductive Unit : Type1 :=
+Inductive Unit : Set :=
     tt : Unit.
 
 Ltac done :=
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 6efd671a8..b1558dab1 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -70,7 +70,7 @@ FST (0; 1)
      : Z
 Nil
      : forall A : Type, list A
-NIL:list nat
+NIL : list nat
      : list nat
 (false && I 3)%bool /\ I 6
      : Prop
@@ -78,7 +78,7 @@ NIL:list nat
      : Z * Z * Z * (Z * Z * Z)
 [|0 * (1, 2, 3); (4, 5, 6) * false|]
      : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
-fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
+fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|} : Z
      : (Z -> Z -> Z -> Z) -> Z
 Init.Nat.add
      : nat -> nat -> nat
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index b1952aecf..f2d144778 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,12 +6,12 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x := A n in ?y ?y0:T n
+fun n : nat => let x := A n in ?y ?y0 : T n
      : forall n : nat, T n
 where
 ?y : [n : nat  x := A n : T n |- ?T0 -> T n] 
 ?y0 : [n : nat  x := A n : T n |- ?T0] 
-fun n : nat => ?y ?y0:T n
+fun n : nat => ?y ?y0 : T n
      : forall n : nat, T n
 where
 ?y : [n : nat |- ?T0 -> T n] 
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 9167c9fcb..dc22b03f2 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -292,3 +292,19 @@ Section foo2.
   Context `{forall A B, Funext A B}.
   Print Universes.
 End foo2.
+
+Module eta.
+Set Universe Polymorphism.
+
+Set Printing Universes.
+
+Axiom admit : forall A, A.
+Record R := {O : Type}.
+
+Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}.
+Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl.
+Definition RLRL' : forall x : R, RL x = RL (RL x).
+  intros. apply eq_refl.
+Qed.
+
+End eta.
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1b396d57b..77339aef4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -402,20 +402,33 @@ let extract_level env evd min tys =
       sign_level env evd ((Anonymous, None, concl) :: ctx)) tys 
   in sup_list min sorts
 
+let is_flexible_sort evd u =
+  match Univ.Universe.level u with
+  | Some l -> Evd.is_flexible_level evd l
+  | None -> false
+
 let inductive_levels env evdref poly arities inds =
-  let destarities = List.map (Reduction.dest_arity env) arities in
-  let levels = List.map (fun (ctx,a) -> 
+  let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
+  let levels = List.map (fun (x,(ctx,a)) -> 
     if a = Prop Null then None
     else Some (univ_of_sort a)) destarities
   in
   let cstrs_levels, min_levels, sizes = 
     CList.split3
-      (List.map2 (fun (_,tys,_) (ctx,du) -> 
+      (List.map2 (fun (_,tys,_) (arity,(ctx,du)) -> 
 	let len = List.length tys in
+	let minlev = Sorts.univ_of_sort du in
 	let minlev =
 	  if len > 1 && not (is_impredicative env du) then
-	    Univ.type0_univ
-	  else Univ.type0m_univ
+	    Univ.sup minlev Univ.type0_univ
+	  else minlev
+	in
+	let minlev =
+	  (** Indices contribute. *)
+	  if Indtypes.is_indices_matter () && List.length ctx > 0 then (
+	    let ilev = sign_level env !evdref ctx in
+	      Univ.sup ilev minlev)
+	  else minlev
 	in
 	let clev = extract_level env !evdref minlev tys in
 	  (clev, minlev, len)) inds destarities)
@@ -425,32 +438,25 @@ let inductive_levels env evdref poly arities inds =
   let levels' = Universes.solve_constraints_system (Array.of_list levels)
     (Array.of_list cstrs_levels) (Array.of_list min_levels)
   in
-  let evd =
-    CList.fold_left3 (fun evd cu (ctx,du) len ->
+  let evd, arities =
+    CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
       if is_impredicative env du then
 	(** Any product is allowed here. *)
-	evd
+	evd, arity :: arities
       else (** If in a predicative sort, or asked to infer the type,
 	       we take the max of:
 	       - indices (if in indices-matter mode)
 	       - constructors
 	       - Type(1) if there is more than 1 constructor
 	   *)
-	let evd = 
-	  (** Indices contribute. *)
-	  if Indtypes.is_indices_matter () && List.length ctx > 0 then (
-	    let ilev = sign_level env !evdref ctx in
-	      Evd.set_leq_sort env evd (Type ilev) du)
-	  else evd
-	in
         (** Constructors contribute. *)
 	let evd = 
 	  if Sorts.is_set du then
 	    if not (Evd.check_leq evd cu Univ.type0_univ) then 
 	      raise (Indtypes.InductiveError Indtypes.LargeNonPropInductiveNotInType)
 	    else evd
-	  else
-	    Evd.set_leq_sort env evd (Type cu) du
+	  else evd
+	    (* Evd.set_leq_sort env evd (Type cu) du *)
 	in
 	let evd = 
 	  if len >= 2 && Univ.is_type0m_univ cu then 
@@ -459,9 +465,19 @@ let inductive_levels env evdref poly arities inds =
 	       land in Prop directly (no informative arguments as well). *)
 	    Evd.set_leq_sort env evd (Prop Pos) du
 	  else evd
-	in evd)
-    !evdref (Array.to_list levels') destarities sizes
-  in evdref := evd; arities
+	in
+	  (* let arity = it_mkProd_or_LetIn (mkType cu) ctx in *\) *)
+	  let duu = Sorts.univ_of_sort du in
+	  let evd =
+	    if not (Univ.is_small_univ duu) && Evd.check_eq evd cu duu then
+	      if is_flexible_sort evd duu then
+		Evd.set_eq_sort env evd (Prop Null) du
+	      else evd
+	    else Evd.set_eq_sort env evd (Type cu) du
+	  in
+	    (evd, arity :: arities))
+    (!evdref,[]) (Array.to_list levels') destarities sizes
+  in evdref := evd; List.rev arities
 
 let check_named (loc, na) = match na with
 | Name _ -> ()
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 98b322af1..9864182a0 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1385,7 +1385,10 @@ let add_infix local ((loc,inf),modifiers) pr sc =
 (**********************************************************************)
 (* Delimiters and classes bound to scopes                             *)
 
-type scope_command = ScopeDelim of string | ScopeClasses of scope_class list
+type scope_command =
+  | ScopeDelim of string
+  | ScopeClasses of scope_class list
+  | ScopeRemove
 
 let load_scope_command _ (_,(scope,dlm)) =
   Notation.declare_scope scope
@@ -1395,6 +1398,7 @@ let open_scope_command i (_,(scope,o)) =
     match o with
     | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
     | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
+    | ScopeRemove -> Notation.remove_delimiters scope
 
 let cache_scope_command o =
   load_scope_command 1 o;
@@ -1420,6 +1424,9 @@ let inScopeCommand : scope_name * scope_command -> obj =
 let add_delimiters scope key =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key))
 
+let remove_delimiters scope =
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove))
+
 let add_class_scope scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 38a377577..f22839f48 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -39,6 +39,7 @@ val add_notation_extra_printing_rule : string -> string -> string -> unit
 (** Declaring delimiter keys and default scopes *)
 
 val add_delimiters : scope_name -> string -> unit
+val remove_delimiters : scope_name -> unit
 val add_class_scope : scope_name -> scope_class list -> unit
 
 (** Add only the interpretation of a notation that already has pa/pp rules *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8d9f8f52c..2af28de98 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -424,7 +424,9 @@ let vernac_syntax_extension locality local =
   let local = enforce_module_locality locality local in
   Metasyntax.add_syntax_extension local
 
-let vernac_delimiters = Metasyntax.add_delimiters
+let vernac_delimiters sc = function
+  | Some lr -> Metasyntax.add_delimiters sc lr
+  | None -> Metasyntax.remove_delimiters sc
 
 let vernac_bind_scope sc cll =
   Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
@@ -1435,6 +1437,15 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
+      optname  = "printing of universes";
+      optkey   = ["Printing";"Universes"];
+      optread  = (fun () -> !Constrextern.print_universes);
+      optwrite = (fun b -> Constrextern.print_universes:=b) }
+     
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
       optname  = "dumping bytecode after compilation";
       optkey   = ["Dump";"Bytecode"];
       optread  = Flags.get_dump_bytecode;