Merge branch 'v8.5'

33 files changed, 310 insertions, 67 deletions

diff --git a/CHANGES b/CHANGES
index a8411a2126..ca31ca2398 100644
--- a/CHANGES
+++ b/CHANGES
@@ -292,7 +292,7 @@ Tools
   added to the load path. (Same behavior as with coq/user-contrib.)
 - coqdep accepts a -dumpgraph option generating a dot file.
 - Makefiles generated through coq_makefile have three new targets "quick"
-  "checkproof" and "vio2vo", allowing respectively to asynchronously compile
+  "checkproofs" and "vio2vo", allowing respectively to asynchronously compile
   the files without playing the proof scripts, asynchronously checking
   that the quickly generated proofs are correct and generating the object
   files from the quickly generated proofs.
diff --git a/COMPATIBILITY b/COMPATIBILITY
index 0d648967f8..eeb0c292b1 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -55,6 +55,13 @@ Potential sources of incompatibilities between Coq V8.4 and V8.5
   (e.g. induction). Extra "Transparent" might have to be added to
   revert opacity of constants.
 
+Type classes.
+
+- When writing an Instance foo : Class A := {| proj := t |} (note the
+  vertical bars), support for typechecking the projections using the
+  type information and switching to proof mode is no longer available.
+  Use { } (without the vertical bars) instead.
+
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
diff --git a/configure.ml b/configure.ml
index 9fa40b0dfd..3aeb324c3b 100644
--- a/configure.ml
+++ b/configure.ml
@@ -77,7 +77,12 @@ let read_lines_and_close fd =
 
 type err = StdErr | StdOut | DevNull
 
+let exe = ref ""  (* Will be set later on, when the suffix is known *)
+
 let run ?(fatal=true) ?(err=StdErr) prog args =
+  let prog = (* Ensure prog ends with exe *)
+    if Str.string_match (Str.regexp ("^.*" ^ !exe ^ "$")) prog 0
+    then prog else (prog ^ !exe) in
   let argv = Array.of_list (prog::args) in
   try
     let out_r,out_w = Unix.pipe () in
@@ -431,7 +436,7 @@ let arch = match !Prefs.arch with
 
 let arch_win32 = (arch = "win32")
 
-let exe = if arch_win32 then ".exe" else ""
+let exe = exe := if arch_win32 then ".exe" else ""; !exe
 let dll = if os_type_win32 then ".dll" else ".so"
 
 (** * VCS
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 1eb40cd36d..11b4f26145 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -560,8 +560,7 @@ The default is to not print synthesizable types.
 \comindex{Print Table Printing Let}}
 
 If an inductive type has just one constructor,
-pattern-matching can be written using {\tt let} ... {\tt :=}
-... {\tt in}~...
+pattern-matching can be written using the first destructuring let syntax.
 
 \begin{quote}
 {\tt Add Printing Let {\ident}.}
@@ -572,7 +571,10 @@ pattern-matching is written using a {\tt let} expression.
 \begin{quote}
 {\tt Remove Printing Let {\ident}.}
 \end{quote}
-This removes {\ident} from this list.
+This removes {\ident} from this list. Note that removing an inductive
+type from this list has an impact only for pattern-matching written using
+\texttt{match}. Pattern-matching explicitly written using a destructuring
+let are not impacted.
 
 \begin{quote}
 {\tt Test Printing Let for {\ident}.}
@@ -630,13 +632,19 @@ it is sensible to the command {\tt Reset}.
 This example emphasizes what the printing options offer.
 
 \begin{coq_example}
+Definition snd (A B:Set) (H:A * B) := match H with
+                                      | pair x y => y
+                                      end.
 Test Printing Let for prod.
-Print fst.
+Print snd.
 Remove Printing Let prod.
 Unset Printing Synth.
 Unset Printing Wildcard.
-Print fst.
+Print snd.
 \end{coq_example}
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
 
 % \subsection{Still not dead old notations}
 
@@ -1051,7 +1059,7 @@ Please note that the questions described here have been subject to
 redesign in Coq v8.5. Former versions of Coq use the same terminology
 to describe slightly different things.
 
-Compiled files (\texttt{.vo} and \texttt{.vi}) store sub-libraries. In
+Compiled files (\texttt{.vo} and \texttt{.vio}) store sub-libraries. In
 order to refer to them inside {\Coq}, a translation from file-system
 names to {\Coq} names is needed. In this translation, names in the
 file system are called {\em physical} paths while {\Coq} names are
diff --git a/ide/coqide.ml b/ide/coqide.ml
index fa64defabd..5aac8f2a18 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -588,13 +588,24 @@ let get_current_word term =
   | Some p -> p
   | None ->
   (** Then look at the current selected word *)
-  if term.script#buffer#has_selection then
-    let (start, stop) = term.script#buffer#selection_bounds in
+  let buf1 = term.script#buffer in
+  let buf2 = term.proof#buffer in
+  let buf3 = term.messages#buffer in
+  if buf1#has_selection then
+    let (start, stop) = buf1#selection_bounds in
+    buf1#get_text ~slice:true ~start ~stop ()
+  else if buf2#has_selection then
+    let (start, stop) = buf2#selection_bounds in
+    buf2#get_text ~slice:true ~start ~stop ()
+  else if buf3#has_selection then
+    let (start, stop) = buf3#selection_bounds in
+    buf3#get_text ~slice:true ~start ~stop ()
+  (** Otherwise try to find the word around the cursor *)
+  else
+    let it = term.script#buffer#get_iter_at_mark `INSERT in
+    let start = find_word_start it in
+    let stop = find_word_end start in
     term.script#buffer#get_text ~slice:true ~start ~stop ()
-  (** Otherwise try to recover the clipboard *)
-  else match Ideutils.cb#text with
-  | Some t -> t
-  | None -> ""
 
 let print_branch c l =
   Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
@@ -838,6 +849,9 @@ let refresh_editor_prefs () =
     sn.command#refresh_font ();
 
     (* Colors *)
+    Tags.set_processing_color (Tags.color_of_string current.processing_color);
+    Tags.set_processed_color (Tags.color_of_string current.processed_color);
+    Tags.set_error_color (Tags.color_of_string current.error_color);
     sn.script#misc#modify_base [`NORMAL, `COLOR clr];
     sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
     sn.messages#misc#modify_base [`NORMAL, `COLOR clr];
@@ -1314,8 +1328,6 @@ let build_ui () =
   refresh_tabs_hook := refresh_notebook_pos;
 
   (* Color configuration *)
-  Tags.set_processing_color (Tags.color_of_string prefs.processing_color);
-  Tags.set_processed_color (Tags.color_of_string prefs.processed_color);
   Tags.Script.incomplete#set_property
     (`BACKGROUND_STIPPLE
       (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
diff --git a/ide/preferences.ml b/ide/preferences.ml
index c850613253..25712f951b 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -503,10 +503,7 @@ let configure ?(apply=(fun () -> ())) () =
       current.processing_color <- Tags.string_of_color processing_button#color;
       current.processed_color <- Tags.string_of_color processed_button#color;
       current.error_color <- Tags.string_of_color error_button#color;
-      !refresh_editor_hook ();
-      Tags.set_processing_color processing_button#color;
-      Tags.set_processed_color processed_button#color;
-      Tags.set_error_color error_button#color
+      !refresh_editor_hook ()
     in
     custom ~label box callback true
   in
diff --git a/ide/session.ml b/ide/session.ml
index 2936321128..dc79fa7905 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -133,6 +133,11 @@ let set_buffer_handlers
     try ignore(buffer#get_mark (`NAME "stop_of_input"))
     with GText.No_such_mark _ -> assert false in
   let get_insert () = buffer#get_iter_at_mark `INSERT in
+  let update_prev it =
+    let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
+    if it#offset < prev#offset then
+      buffer#move_mark (`NAME "prev_insert") ~where:it
+  in
   let debug_edit_zone () = if false (*!Minilib.debug*) then begin
     buffer#remove_tag Tags.Script.edit_zone
       ~start:buffer#start_iter ~stop:buffer#end_iter;
@@ -147,6 +152,7 @@ let set_buffer_handlers
   let insert_cb it s = if String.length s = 0 then () else begin
     Minilib.log ("insert_cb " ^ string_of_int it#offset);
     let text_mark = add_mark it in
+    let () = update_prev it in
     if it#has_tag Tags.Script.to_process then
       cancel_signal "Altering the script being processed in not implemented"
     else if it#has_tag Tags.Script.read_only then
@@ -160,9 +166,9 @@ let set_buffer_handlers
     end end in
   let delete_cb ~start ~stop =
     Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
-    cur_action := new_action_id ();
     let min_iter, max_iter =
       if start#compare stop < 0 then start, stop else stop, start in
+    let () = update_prev min_iter in
     let text_mark = add_mark min_iter in
     let rec aux min_iter =
       if min_iter#equal max_iter then ()
@@ -465,7 +471,7 @@ let build_layout (sn:session) =
       message_frame#misc#show ();
       detachable#show);
     detachable#button#misc#hide ();
-    lbl in
+    detachable, lbl in
   let session_tab = GPack.hbox ~homogeneous:false () in
   let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
     ~packing:session_tab#pack () in
@@ -496,9 +502,17 @@ let build_layout (sn:session) =
   sn.command#pack_in (session_paned#pack2 ~shrink:false ~resize:false);
   script_scroll#add sn.script#coerce;
   proof_scroll#add sn.proof#coerce;
-  ignore(add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce);
-  let label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
-  ignore(add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce);
+  let detach, _ = add_msg_page 0 sn.tab_label#text "Messages" sn.messages#coerce in
+  let _, label = add_msg_page 1 sn.tab_label#text "Errors" sn.errpage#coerce in
+  let _, _ = add_msg_page 2 sn.tab_label#text "Jobs" sn.jobpage#coerce in
+  (** When a message is received, focus on the message pane *)
+  let _ =
+    sn.messages#connect#pushed ~callback:(fun _ _ ->
+      let num = message_frame#page_num detach#coerce in
+      if 0 <= num then message_frame#goto_page num
+    )
+  in
+  (** When an error occurs, paint the error label in red *)
   let txt = label#text in
   let red s = "<span foreground=\"#FF0000\">" ^ s ^ "</span>" in
   sn.errpage#on_update ~callback:(fun l ->
diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml
index 9acda53fc3..09f1d44535 100644
--- a/ide/wg_MessageView.ml
+++ b/ide/wg_MessageView.ml
@@ -6,9 +6,25 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+class type message_view_signals =
+object
+  inherit GObj.misc_signals
+  inherit GUtil.add_ml_signals
+  method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+end
+
+class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals =
+object
+  val after = false
+  inherit GObj.misc_signals obj
+  inherit GUtil.add_ml_signals obj [pushed#disconnect]
+  method pushed ~callback = pushed#connect ~after ~callback:(fun (lvl, s) -> callback lvl s)
+end
+
 class type message_view =
   object
     inherit GObj.widget
+    method connect : message_view_signals
     method clear : unit
     method add : string -> unit
     method set : string -> unit
@@ -38,6 +54,11 @@ let message_view () : message_view =
   object (self)
     inherit GObj.widget box#as_widget
 
+    val push = new GUtil.signal ()
+
+    method connect =
+      new message_view_signals_impl box#as_widget push
+
     method clear =
       buffer#set_text ""
 
@@ -49,7 +70,8 @@ let message_view () : message_view =
       in
       if msg <> "" then begin
         buffer#insert ~tags msg;
-        buffer#insert ~tags "\n"
+        buffer#insert ~tags "\n";
+        push#call (level, msg)
       end
 
     method add msg = self#push Pp.Notice msg
diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli
index cd3f00c97d..4dcd7306ba 100644
--- a/ide/wg_MessageView.mli
+++ b/ide/wg_MessageView.mli
@@ -6,9 +6,17 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+class type message_view_signals =
+object
+  inherit GObj.misc_signals
+  inherit GUtil.add_ml_signals
+  method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id
+end
+
 class type message_view =
   object
     inherit GObj.widget
+    method connect : message_view_signals
     method clear : unit
     method add : string -> unit
     method set : string -> unit
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 7e7a311ed0..a33f2c591c 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -9,6 +9,7 @@
 class type proof_view =
   object
     inherit GObj.widget
+    method buffer : GText.buffer
     method refresh : unit -> unit
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
@@ -176,6 +177,7 @@ let proof_view () =
     ~highlight_matching_brackets:true
     ~tag_table:Tags.Proof.table ()
   in
+  let text_buffer = new GText.buffer buffer#as_buffer in
   let view = GSourceView2.source_view
     ~source_buffer:buffer ~editable:false ~wrap_mode:`WORD ()
   in
@@ -186,6 +188,8 @@ let proof_view () =
     val mutable goals = None
     val mutable evars = None
 
+    method buffer = text_buffer
+
     method clear () = buffer#set_text ""
 
     method set_goals gls = goals <- gls
diff --git a/ide/wg_ProofView.mli b/ide/wg_ProofView.mli
index 1fbf9900ca..c5e042ea52 100644
--- a/ide/wg_ProofView.mli
+++ b/ide/wg_ProofView.mli
@@ -9,6 +9,7 @@
 class type proof_view =
   object
     inherit GObj.widget
+    method buffer : GText.buffer
     method refresh : unit -> unit
     method clear : unit -> unit
     method set_goals : Interface.goals option -> unit
diff --git a/interp/modintern.ml b/interp/modintern.ml
index fdc6e609bc..bf0b2f9800 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,7 +61,9 @@ let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
       WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
-      WithDef (fqid,fst (interp_constr env Evd.empty c)) (*FIXME*)
+    let c, ectx = interp_constr env (Evd.from_env env) c in
+    let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in
+      WithDef (fqid,(c,ctx))
 
 let loc_of_module = function
   | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index bec521227b..cef920c6a5 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -202,7 +202,7 @@ type ('ty,'a) functorize =
 
 type with_declaration =
   | WithMod of Id.t list * module_path
-  | WithDef of Id.t list * constr
+  | WithDef of Id.t list * constr Univ.in_universe_context
 
 type module_alg_expr =
   | MEident of module_path
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 97c1d1fdfa..99d353aae6 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -54,7 +54,7 @@ let rec rebuild_mp mp l =
 
 let (+++) = Univ.Constraint.union
 
-let rec check_with_def env struc (idl,c) mp equiv =
+let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
   let lab,idl = match idl with
     | [] -> assert false
     | id::idl -> Label.of_id id, idl
@@ -74,30 +74,33 @@ let rec check_with_def env struc (idl,c) mp equiv =
 	 as long as they have the right type *)
       let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
       let env' = Environ.add_constraints ccst env' in
+      let newus, cst = Univ.UContext.dest ctx in
+      let env' = Environ.add_constraints cst env' in
       let c',cst = match cb.const_body with
 	| Undef _ | OpaqueDef _ ->
 	  let j = Typeops.infer env' c in
 	  let typ = Typeops.type_of_constant_type env' cb.const_type in
-	  let cst = Reduction.infer_conv_leq env' (Environ.universes env')
+	  let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 	    j.uj_type typ in
-	  j.uj_val,cst
+	  j.uj_val,cst' +++ cst
 	| Def cs ->
-	  let cst = Reduction.infer_conv env' (Environ.universes env') c
+	  let cst' = Reduction.infer_conv env' (Environ.universes env') c
 	    (Mod_subst.force_constr cs) in
 	  let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
-	    if cb.const_polymorphic then cst
-	    else ccst +++ cst 
+	    if cb.const_polymorphic then cst' +++ cst
+	    else cst' +++ cst
 	  in
             c, cst
       in
       let def = Def (Mod_subst.from_val c') in
+      let ctx' = Univ.UContext.make (newus, cst) in
       let cb' =
 	{ cb with
 	  const_body = def;
-	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def) }
-	  (* const_universes = Future.from_val cst } *)
+	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
+	  const_universes = ctx' }
       in
-      before@(lab,SFBconst(cb'))::after, c', cst
+      before@(lab,SFBconst(cb'))::after, c', ctx'
     else
       (* Definition inside a sub-module *)
       let mb = match spec with
@@ -108,7 +111,7 @@ let rec check_with_def env struc (idl,c) mp equiv =
       | Abstract ->
         let struc = Modops.destr_nofunctor mb.mod_type in
         let struc',c',cst =
-          check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta
+          check_with_def env' struc (idl,(c,ctx)) (MPdot(mp,lab)) mb.mod_delta
         in
         let mb' = { mb with
           mod_type = NoFunctor struc';
@@ -204,8 +207,8 @@ let check_with env mp (sign,alg,reso,cst) = function
   |WithDef(idl,c) ->
     let struc = destr_nofunctor sign in
     let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
-    let alg' = mk_alg_with alg (WithDef (idl,c')) in
-    (NoFunctor struc'),alg',reso, cst+++cst'
+    let alg' = mk_alg_with alg (WithDef (idl,(c',cst'))) in
+    (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst')
   |WithMod(idl,mp1) as wd ->
     let struc = destr_nofunctor sign in
     let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 392e667b8e..83be03ffd8 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -177,9 +177,9 @@ let subst_with_body sub = function
   |WithMod(id,mp) as orig ->
     let mp' = subst_mp sub mp in
     if mp==mp' then orig else WithMod(id,mp')
-  |WithDef(id,c) as orig ->
+  |WithDef(id,(c,ctx)) as orig ->
     let c' = subst_mps sub c in
-    if c==c' then orig else WithDef(id,c')
+    if c==c' then orig else WithDef(id,(c',ctx))
 
 let rec subst_structure sub do_delta sign =
   let subst_body ((l,body) as orig) = match body with
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 8246df283b..3bb029a888 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -157,7 +157,7 @@ GEXTEND Gram
       ] ]
   ;
   universe:
-    [ [ "max("; ids = LIST1 ident SEP ","; ")" -> ids
+    [ [ IDENT "max"; "("; ids = LIST1 ident SEP ","; ")" -> ids
       | id = ident -> [id]
       ] ]
   ;
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 42e69d342e..90ee6d0ef1 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -235,7 +235,7 @@ let rec extract_structure_spec env mp = function
 
 and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MEident mp -> Visit.add_mp_all mp; MTident mp
-  | MEwith(me',WithDef(idl,c))->
+  | MEwith(me',WithDef(idl,(c,ctx)))->
       let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in
       let mt = extract_mexpr_spec env mp1 (me_struct,me') in
       (match extract_with_type env' c with (* cb may contain some kn *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 5aa72c90ac..921609aae3 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -186,6 +186,7 @@ let noccur_evar env evd evk c =
       (match pi2 (Environ.lookup_rel (i-k) env) with
        | None -> ()
        | Some b -> occur_rec k (lift i b))
+  | Proj (p,c) -> occur_rec k (Retyping.expand_projection env evd p c [])
   | _ -> iter_constr_with_binders succ occur_rec k c
   in
   try occur_rec 0 c; true with Occur -> false
diff --git a/stm/stm.ml b/stm/stm.ml
index 96a11d306d..693c673b40 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1554,6 +1554,7 @@ let async_policy () =
 let delegate name =
   let time = get_hint_bp_time name in
   time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio
+              || !Flags.async_proofs_full
 
 let collect_proof keep cur hd brkind id =
  prerr_endline ("Collecting proof ending at "^Stateid.to_string id);
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index f00ecf8feb..9a64b03fd1 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -210,6 +210,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   end in
   let avoid = ref [] in
   let { sigma=sigma } = Proof.V82.subgoals pf in
+  let sigma = Evd.nf_constraints sigma in
   let rec fill_holes c =
     match kind_of_term c with
     | Evar (e,args) ->
@@ -222,13 +223,13 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   in
   let c = fill_holes pfterm in
   (* warning: side-effect on ownSign *)
-  let invProof = it_mkNamedLambda_or_LetIn c !ownSign
-  in
-  invProof
+  let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
+  let p = Evarutil.nf_evars_universes sigma invProof in
+    p, Evd.universe_context sigma
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
-  let invProof = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:true (*FIXME*) invProof in
+  let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
+  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) ~univs:ctx invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
 
@@ -236,7 +237,8 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
  * inv_op = InvNoThining (derives de semi inversion lemma) *)
 
 let add_inversion_lemma_exn na com comsort bool tac =
-  let env = Global.env () and evd = ref Evd.empty in
+  let env = Global.env () in
+  let evd = ref (Evd.from_env env) in
   let c = Constrintern.interp_type_evars env evd com in
   let sigma, sort = Pretyping.interp_sort !evd comsort in
   try
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 215713d981..ab71f5f2e7 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -176,6 +176,13 @@ let coerce_to_evaluable_ref env v =
     let id = out_gen (topwit wit_var) v in
     if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id
     else fail ()
+  else if has_type v (topwit wit_ref) then
+    let open Globnames in
+    let r = out_gen (topwit wit_ref) v in
+    match r with
+    | VarRef var -> EvalVarRef var
+    | ConstRef c -> EvalConstRef c
+    | IndRef _ | ConstructRef _ -> fail ()
   else
     let ev = match Value.to_constr v with
     | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9265328a47..04df3b8cda 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -425,7 +425,7 @@ let pf_reduce_decl redfun where (id,c,ty) gl =
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
       (id,None,redfun' ty)
   | Some b ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -522,7 +522,7 @@ let pf_e_reduce_decl redfun where (id,c,ty) gl =
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma, ty' = redfun sigma ty in
       sigma, (id,None,ty')
   | Some b ->
@@ -565,12 +565,16 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where (id,c,ty) env
   match c with
   | None ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str "has no value.");
+	errorlabstrm "" (pr_id id ++ str " has no value.");
     let sigma',ty' = redfun false env sigma ty in
       sigma', (id,None,ty')
   | Some b ->
-      let sigma',b' = if where != InHypTypeOnly then redfun true env sigma b else sigma, b in
-      let sigma',ty' = if where != InHypValueOnly then redfun false env sigma ty else sigma', ty in
+      let sigma',b' = 
+	if where != InHypTypeOnly then redfun true env sigma b else sigma, b 
+      in
+      let sigma',ty' = 
+	if where != InHypValueOnly then redfun false env sigma' ty else sigma', ty 
+      in
 	sigma', (id,Some b',ty')
 
 let e_change_in_hyp redfun (id,where) =
diff --git a/test-suite/bugs/closed/2590.v b/test-suite/bugs/closed/2590.v
new file mode 100644
index 0000000000..e594e96936
--- /dev/null
+++ b/test-suite/bugs/closed/2590.v
@@ -0,0 +1,19 @@
+Require Import Relation_Definitions RelationClasses Setoid SetoidClass.
+
+Section Bug.
+
+  Context {A : Type} (R : relation A).
+  Hypothesis pre : PreOrder R.
+  Context `{SA : Setoid A}.
+
+  Goal True.
+  set (SA' := SA).
+    assert ( forall SA0 : Setoid A,
+               @PartialOrder A (@equiv A SA0) (@setoid_equiv A SA0) R pre ).
+    rename SA into SA0.
+    intro SA.
+    admit.
+    admit.
+Qed.
+End Bug.
+
diff --git a/test-suite/bugs/closed/2775.v b/test-suite/bugs/closed/2775.v
new file mode 100644
index 0000000000..f1f384bdf7
--- /dev/null
+++ b/test-suite/bugs/closed/2775.v
@@ -0,0 +1,6 @@
+Inductive typ : forall (T:Type), list T ->  Type -> Prop :=
+  | Get : forall (T:Type) (l:list T), typ T l T.
+
+
+Derive Inversion inv with 
+(forall (X: Type) (y: list nat), typ nat y X)  Sort Prop.
diff --git a/test-suite/bugs/closed/3309.v b/test-suite/bugs/closed/3309.v
index fcebdec728..9e12b990b7 100644
--- a/test-suite/bugs/closed/3309.v
+++ b/test-suite/bugs/closed/3309.v
@@ -315,12 +315,14 @@ Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) :  hrel (@setq
 intros; exact (@quotrel _ _).
 Defined.
 
+(* Unset Kernel Term Sharing. *)
+
 Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit.
 
 Definition ispartlbinopabmonoidfracrel_type : Type :=
   forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ), 
     @abmonoidfracrel X A ( ( admit + z ) )admit.
 
-Axiom ispartlbinopabmonoidfracrel : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
+Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel' : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in
                                       ispartlbinopabmonoidfracrel_type in exact t)$.
 
diff --git a/test-suite/bugs/closed/3560.v b/test-suite/bugs/closed/3560.v
new file mode 100644
index 0000000000..65ce4fb6b0
--- /dev/null
+++ b/test-suite/bugs/closed/3560.v
@@ -0,0 +1,15 @@
+
+(* File reduced by coq-bug-finder from original input, then from 6236 lines to 1049 lines, then from 920 lines to 209 lines, then from 179 lines to 30 lines *)
+(* coqc version trunk (August 2014) compiled on Aug 31 2014 10:12:32 with OCaml 4.01.0
+   coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (437b91a3ffd7327975a129b95b24d3f66ad7f3e4) *)
+
+Set Primitive Projections.
+Set Implicit Arguments.
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Notation "x * y" := (prod x y) : type_scope.
+Record Equiv A B := { equiv_fun :> A -> B ; equiv_isequiv : forall P, P equiv_fun }.
+Goal forall (A B : Type) (C : Type), Equiv (A -> B -> C) (A * B -> C).
+Proof.
+  intros.
+  exists (fun u => fun x => u (fst x) (snd x)).
+Abort.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3783.v b/test-suite/bugs/closed/3783.v
new file mode 100644
index 0000000000..33ca9651a5
--- /dev/null
+++ b/test-suite/bugs/closed/3783.v
@@ -0,0 +1,32 @@
+Fixpoint exp (n : nat) (T : Set)
+  := match n with
+       | 0 => T
+       | S n' => exp n' (T * T)
+     end.
+Definition big := Eval compute in exp 13 nat.
+Module NonPrim.
+  Unset Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Time cbv beta in y. (* 0s *)
+    admit.
+  Defined.
+End NonPrim.
+Module Prim.
+  Set Primitive Projections.
+  Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
+  Definition x : sigT (fun x => x).
+  Proof.
+    exists big; admit.
+  Defined.
+  Goal True.
+    pose ((fun y => y = y) (projT1 _ x)) as y.
+    Timeout 1 cbv beta in y. (* takes around 2s.  Grows with the value passed to [exp] above *)
+    admit.
+  Defined.
+End Prim.
\ No newline at end of file
diff --git a/test-suite/bugs/opened/3786.v b/test-suite/bugs/closed/3786.v
index 5a1241151c..fd3bd7bd76 100644
--- a/test-suite/bugs/opened/3786.v
+++ b/test-suite/bugs/closed/3786.v
@@ -26,15 +26,7 @@ Definition sumUniqueImpl (ls : list nat)
 Proof.
   eexists.
   match goal with
-    | [ |- refine ?a ?b ] => let a' := eval hnf in a in refine (_ : refine a' b)
-  end;
-  try setoid_rewrite (@finite_set_handle_cardinal).
-  Undo.
-  match goal with
     | [ |- refine ?a ?b ] => let a' := eval hnf in a in change (refine a' b)
   end.
-  try setoid_rewrite (@finite_set_handle_cardinal). (* Anomaly: Uncaught exception Invalid_argument("decomp_pointwise").
-Please report. *)
-  instantiate (1 := admit).
-  admit.
-Defined.
+  try setoid_rewrite (@finite_set_handle_cardinal).
+Abort.
diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v
new file mode 100644
index 0000000000..7c3cc6b791
--- /dev/null
+++ b/test-suite/bugs/closed/3881.v
@@ -0,0 +1,35 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 2236 lines to 1877 lines, then from 1652 lines to 160 lines, then from 102 lines to 34 lines *)
+(* coqc version trunk (December 2014) compiled on Dec 23 2014 22:6:43 with OCaml 4.01.0
+   coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (90ed6636dea41486ddf2cc0daead83f9f0788163) *)
+Generalizable All Variables.
+Require Import Coq.Init.Notations.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Axiom admit : forall {T}, T.
+Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity).
+Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *)
+Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope.
+Arguments eq_refl {_ _}.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end.
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A ; eisretr : forall x, f (equiv_inv x) = x }.
+Arguments eisretr {A B} f {_} _.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'").
+Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (g o f) | 1000 := admit.
+Definition isequiv_homotopic {A B} (f : A -> B) (g : A -> B) `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g := admit.
+Global Instance isequiv_inverse {A B} (f : A -> B) {feq : IsEquiv f} : IsEquiv f^-1 | 10000 := admit.
+Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} `{IsEquiv A B f} `{IsEquiv A C (g o f)} : IsEquiv g.
+Proof.
+  pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H
+                                    (fun b => ap g (eisretr f b))) as k.
+  revert k.
+  let x := match goal with |- let k := ?x in _ => constr:x end in
+  intro k; clear k;
+  pose (x _).
+  pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _
+                           (fun b => ap g (eisretr f b))).
+  Undo. 
+  apply (@isequiv_homotopic _ _ ((g o f) o f^-1) g _
+                           (fun b => ap g (eisretr f b))).
+Qed.
+  
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3978.v b/test-suite/bugs/closed/3978.v
new file mode 100644
index 0000000000..26e021e719
--- /dev/null
+++ b/test-suite/bugs/closed/3978.v
@@ -0,0 +1,27 @@
+Require Import Structures.OrderedType.  
+Require Import Structures.OrderedTypeEx.
+
+Module Type M. Parameter X : Type.      
+
+Declare Module Export XOrd : OrderedType
+  with Definition t := X
+  with Definition eq := @Logic.eq X.
+End M.
+
+Module M' : M.
+  Definition X := nat.
+
+  Module XOrd := Nat_as_OT.
+End M'.
+
+Module Type MyOt.
+  Parameter t : Type.
+  Parameter eq : t -> t -> Prop.
+End MyOt.
+
+Module Type M2. Parameter X : Type.      
+
+Declare Module Export XOrd : MyOt
+  with Definition t := X
+  with Definition eq := @Logic.eq X.
+End M2.
diff --git a/test-suite/bugs/closed/4031.v b/test-suite/bugs/closed/4031.v
new file mode 100644
index 0000000000..2b8641ebb0
--- /dev/null
+++ b/test-suite/bugs/closed/4031.v
@@ -0,0 +1,14 @@
+Definition something (P:Type) (e:P) := e.
+
+Inductive myunit : Set := mytt.
+  (* Proof below works when definition is in Type,
+     however builtin types such as unit are in Set. *)
+
+Lemma demo_hide_generic : 
+   let x := mytt in x = x.
+Proof.
+  intros.
+  change mytt with (@something _ mytt) in x.
+  subst x. (* Proof works if this line is removed *)
+  reflexivity.
+Qed.
\ No newline at end of file
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 9341f2f70a..5429e6608d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -879,7 +879,9 @@ let explain_label_already_declared l =
   str ("The label "^Label.to_string l^" is already declared.")
 
 let explain_application_to_not_path _ =
-  str "Application of modules is restricted to paths."
+  strbrk "A module cannot be applied to another module application or " ++
+  strbrk "with-expression; you must give a name to the intermediate result " ++
+  strbrk "module first."
 
 let explain_not_a_functor () =
   str "Application of a non-functor."
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index d4d4456994..e9b5e8f84a 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -47,6 +47,7 @@ let print_usage_channel co command =
 \n  -require f             load Coq object file f.vo and import it (Require f.)\
 \n  -compile f             compile Coq file f.v (implies -batch)\
 \n  -compile-verbose f     verbosely compile Coq file f.v (implies -batch)\
+\n  -quick                 quickly compile .v files to .vio files (skip proofs)\
 \n\
 \n  -where                 print Coq's standard library location and exit\
 \n  -config                print Coq's configuration information and exit\