Merge remote-tracking branch 'forge/v8.5'

24 files changed, 462 insertions, 89 deletions

diff --git a/checker/votour.ml b/checker/votour.ml
index 7c954d6f9..01965bb4b 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -203,12 +203,45 @@ let rec visit v o pos =
 
 (** Loading the vo *)
 
+type header = {
+  magic : string;
+  (** Magic number of the marshaller *)
+  length : int;
+  (** Size on disk in bytes *)
+  size32 : int;
+  (** Size in words when loaded on 32-bit systems *)
+  size64 : int;
+  (** Size in words when loaded on 64-bit systems *)
+  objects : int;
+  (** Number of blocks defined in the marshalled structure *)
+}
+
+let dummy_header = {
+  magic = "\000\000\000\000";
+  length = 0;
+  size32 = 0;
+  size64 = 0;
+  objects = 0;
+}
+
+let parse_header chan =
+  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 }
+
 type segment = {
   name : string;
   mutable pos : int;
   typ : Values.value;
+  mutable header : header;
 }
 
+let make_seg name typ = { name; typ; pos = 0; header = dummy_header }
+
 let visit_vo f =
   Printf.printf "\nWelcome to votour !\n";
   Printf.printf "Enjoy your guided tour of a Coq .vo or .vi file\n";
@@ -216,11 +249,11 @@ let visit_vo f =
   Printf.printf
     "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!";
   let segments = [|
-    {name="library"; pos=0; typ=Values.v_lib};
-    {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; 
-    {name="discharging info"; pos=0; typ=Opt Any};
-    {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg};
-    {name="opaque proofs"; pos=0; typ=Values.v_opaques}; 
+    make_seg "library" Values.v_lib;
+    make_seg "univ constraints of opaque proofs" Values.v_univopaques;
+    make_seg "discharging info" (Opt Any);
+    make_seg "STM tasks" (Opt Values.v_stm_seg);
+    make_seg "opaque proofs" Values.v_opaques;
   |] in
   while true do
     let ch = open_in_bin f in
@@ -229,13 +262,16 @@ let visit_vo f =
     for i=0 to Array.length segments - 1 do
       let pos = input_binary_int ch in
       segments.(i).pos <- pos_in ch;
+      let header = parse_header ch in
+      segments.(i).header <- header;
       seek_in ch pos;
       ignore(Digest.input ch);
     done;
     Printf.printf "The file has %d segments, choose the one to visit:\n"
       (Array.length segments);
-    Array.iteri (fun i { name; pos } ->
-      Printf.printf "  %d: %s, starting at byte %d\n" i name pos)
+    Array.iteri (fun i { name; pos; header } ->
+      let size = if Sys.word_size = 64 then header.size64 else header.size32 in
+      Printf.printf "  %d: %s, starting at byte %d (size %iw)\n" i name pos size)
       segments;
     Printf.printf "# %!";
     let l = read_line () in
diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh
new file mode 100755
index 000000000..73e1fdbeb
--- /dev/null
+++ b/dev/make-installer-win64.sh
@@ -0,0 +1,26 @@
+#!/bin/sh
+
+NSIS="$BASE/NSIS/makensis"
+ZIP=_make.zip
+URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download
+URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download
+
+[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no
+make -j2 coqide
+mkdir -p bin32
+cp bin/* bin32/
+make clean
+make archclean
+( . ${BASE}_64/environ; ./configure -prefix ./ -with-doc no; make -j2; make ide/coqidetop.cmxs )
+cp bin32/coqide* bin/
+if [ ! -e bin/make.exe ]; then
+  wget -O $ZIP $URL1 && 7z x $ZIP "bin/*"
+  wget -O $ZIP $URL2 && 7z x $ZIP "bin/*"
+  rm -rf $ZIP
+fi
+VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
+cd dev/nsis
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+echo Installer:
+ls -h $PWD/*exe
+cd ../..
diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex
index 797bf2434..47dc1ac1a 100644
--- a/doc/refman/AsyncProofs.tex
+++ b/doc/refman/AsyncProofs.tex
@@ -18,13 +18,11 @@ on small sets of short files.
 This feature has some technical limitations that may make it unsuitable for
 some use cases.
 
-For example, in interactive mode, errors coming from the kernel of Coq are
-signaled late.  The most notable type of errors belonging to this category are
-universe inconsistencies or unsatisfied guardedness conditions for fixpoints
-built using tactics.
+For example, in interactive mode, some errors coming from the kernel of Coq
+are signaled late.  The type of errors belonging to this category
+are universe inconsistencies.
 
-Last, at the time of writing, only opaque proofs (ending with \texttt{Qed}) can be
-processed asynchronously.
+Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously.
 
 \subsection{Proof annotations}
 
diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang
index 4c488ae89..7cfc16701 100644
--- a/ide/coq-ssreflect.lang
+++ b/ide/coq-ssreflect.lang
@@ -190,6 +190,7 @@
 	  <keyword>Eval</keyword>
 	  <keyword>Load</keyword>
 	  <keyword>Undo</keyword>
+          <keyword>Restart</keyword>
 	  <keyword>Goal</keyword>
 	  <keyword>Print</keyword>
 	  <keyword>Save</keyword>
diff --git a/ide/coq.lang b/ide/coq.lang
index 35dff85e6..c65432bdb 100644
--- a/ide/coq.lang
+++ b/ide/coq.lang
@@ -161,6 +161,7 @@
           <keyword>Print</keyword>
           <keyword>Eval</keyword>
           <keyword>Undo</keyword>
+          <keyword>Restart</keyword>
           <keyword>Opaque</keyword>
           <keyword>Transparent</keyword>
         </context>
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index af728471f..2387d65c3 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -655,8 +655,6 @@ object(self)
       buffer#remove_tag Tags.Script.unjustified ~start ~stop;
       buffer#remove_tag Tags.Script.tooltip ~start ~stop;
       buffer#remove_tag Tags.Script.to_process ~start ~stop;
-      buffer#remove_tag Tags.Script.error ~start ~stop;
-      buffer#remove_tag Tags.Script.error_bg ~start ~stop;
       buffer#move_mark ~where:start (`NAME "start_of_input")
     end;
     List.iter (fun { start } -> buffer#delete_mark start) seg;
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 1f3fa3ed3..69d460b01 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -140,20 +140,22 @@ let display mode (view : #GText.view_skel) goals hints evars =
       view#buffer#insert "No more subgoals."
     | [], [], [], _ :: _ ->
       (* A proof has been finished, but not concluded *)
-      view#buffer#insert "No more subgoals but non-instantiated existential variables:\n\n";
+      view#buffer#insert "No more subgoals, but there are non-instantiated existential variables:\n\n";
       let iter evar =
         let msg = Printf.sprintf "%s\n" evar.Interface.evar_info in
         view#buffer#insert msg
       in
-      List.iter iter evars
+      List.iter iter evars;
+      view#buffer#insert "\nYou can use Grab Existential Variables."
     | [], [], _, _ ->
       (* The proof is finished, with the exception of given up goals. *)
-      view#buffer#insert "No more, however there are goals you gave up. You need to go back and solve them:\n\n";
+      view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n";
       let iter goal =
         let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
         view#buffer#insert msg
       in
-      List.iter iter given_up_goals
+      List.iter iter given_up_goals;
+      view#buffer#insert "\nYou need to go back and solve them."
     | [], _, _, _ ->
       (* All the goals have been resolved but those on the shelf. *)
       view#buffer#insert "All the remaining goals are on the shelf:\n\n";
@@ -168,11 +170,7 @@ let display mode (view : #GText.view_skel) goals hints evars =
       let goal_str index = Printf.sprintf
         "______________________________________(%d/%d)\n" index total
       in
-      let vb, pl = if total = 1 then "is", "" else "are", "s" in
-      let msg = Printf.sprintf "This subproof is complete, but there %s still %d \
-        unfocused goal%s:\n\n" vb total pl
-      in
-      let () = view#buffer#insert msg in
+      view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n";
       let iter i goal =
         let () = view#buffer#insert (goal_str (succ i)) in
         let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index c7b18b900..f06275862 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -12,6 +12,7 @@
 #define _COQ_CAML_GC_
 #include <caml/mlvalues.h>
 #include <caml/alloc.h>
+#include <caml/memory.h>
 
 typedef void (*scanning_action) (value, value *);
 
@@ -24,12 +25,22 @@ CAMLextern void minor_collection (void);
 #define Caml_white (0 << 8)
 #define Caml_black (3 << 8)
 
+#ifdef HAS_OCP_MEMPROF
+
+/*  This code is necessary to make the OCamlPro memory profiling branch of
+    OCaml compile. */
+
+#define Make_header(wosize, tag, color)                                 \
+  caml_make_header(wosize, tag, color)
+
+#else
+
 #define Make_header(wosize, tag, color)                                 \
   (((header_t) (((header_t) (wosize) << 10)                             \
 		+ (color)                                               \
 		+ (tag_t) (tag)))   					\
    )
-
+#endif
 
 #define Alloc_small(result, wosize, tag) do{                            \
   young_ptr -= Bhsize_wosize (wosize);                                  \
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ada7ae737..f56b6f83e 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2015,9 +2015,13 @@ let rec compile_deps env sigma prefix ~interactive init t =
         || (Cmap_env.mem c const_updates)
       then init
       else
-      let comp_stack, (mind_updates, const_updates) = match cb.const_body with
-        | Def t ->
+      let comp_stack, (mind_updates, const_updates) =
+	match cb.const_proj, cb.const_body with
+        | None, Def t ->
 	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+	| Some pb, _ ->
+	   let mind = pb.proj_ind in
+	   compile_mind_deps env prefix ~interactive init mind
         | _ -> init
       in
       let code, name =
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 4be8ced54..ce9e4e2b0 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -102,22 +102,23 @@ let compile_library dir code fn =
   r
 
 (* call_linker links dynamically the code for constants in environment or a  *)
-(* conversion test. Silently fails if the file does not exist in bytecode    *)
-(* mode, since the standard library is not compiled to bytecode with default *)
-(* settings.                                                                 *)
+(* conversion test. *)
 let call_linker ?(fatal=true) prefix f upds =
   rt1 := dummy_value ();
   rt2 := dummy_value ();
-  if Dynlink.is_native || Sys.file_exists f then
+  if not (Sys.file_exists f) then
+    let msg = "Cannot find native compiler file " ^ f in
+    if fatal then Errors.error msg
+    else Pp.msg_warning (Pp.str msg)
+  else
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
     register_native_file prefix
-   with | Dynlink.Error e ->
-          let msg = "Dynlink error, " ^ Dynlink.error_message e in
-          if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
-        | e when Errors.noncritical e ->
-          if fatal then anomaly (Errors.print e)
-	  else Pp.msg_warning (Errors.print_no_report e));
+   with Dynlink.Error e as exn ->
+     let exn = Errors.push exn in
+     let msg = "Dynlink error, " ^ Dynlink.error_message e in
+     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
+     else Pp.msg_warning (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
diff --git a/library/universes.ml b/library/universes.ml
index 3a7a76907..16e6ebb02 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -739,15 +739,14 @@ let minimize_univ_variables ctx us algs left right cstrs =
   let rec instance (ctx', us, algs, insts, cstrs as acc) u =
     let acc, left = 
       try let l = LMap.find u left in
-	    List.fold_left (fun (acc, left') (d, l) -> 
-	      let acc', (enf,alg,l') = aux acc l in
-		(* if alg then assert(not alg); *)
-		let l' = 
-		  if enf then Universe.make l 
-		  else l' 
-		(* match Universe.level l' with Some _ -> l' | None -> Universe.make l  *)
-		in
-		  acc', (d, l') :: left') (acc, []) l
+	    List.fold_left
+	      (fun (acc, left') (d, l) -> 
+	       let acc', (enf,alg,l') = aux acc l in
+	       let l' = 
+		 if enf then Universe.make l 
+		 else l' 
+	       in acc', (d, l') :: left')
+	      (acc, []) l
       with Not_found -> acc, []
     and right =
       try Some (LMap.find u right)
@@ -755,24 +754,21 @@ let minimize_univ_variables ctx us algs left right cstrs =
     in
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
-      if alg then
-	 (* u is algebraic and has no upper bound constraints: we
-	    instantiate it with it's lower bound, if any *)
-	 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 *) 
-	  (* u is not algebraic but has no upper bounds,
-	     we instantiate it with its lower bound if it is a 
-	     different level, otherwise we keep it. *)
-	  if not (Level.equal l u) && not (LSet.mem l algs) then
-	    (* if right = None then. Should check that u does not 
-	       have upper constraints that are not already in right *)
-	      instantiate_with_lbound u lbound false false acc
-	    (* else instantiate_with_lbound u lbound false true acc *)
-	  else
-	    (* assert false: l can't be alg *)
-	    acc, (true, false, lbound)
+	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
+	else (* u is non algebraic *)
+	  match Universe.level lbound with
+	  | Some l -> (* The lowerbound is directly a level *) 
+	     (* u is not algebraic but has no upper bounds,
+  	        we instantiate it with its lower bound if it is a 
+	        different level, otherwise we keep it. *)
+	     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
+	     else acc, (true, false, lbound)
 	| None -> 
 	  try 
 	    (* if right <> None then raise Not_found; *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 09059b410..e8a1b512c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -249,7 +249,8 @@ GEXTEND Gram
     [ [ IDENT "Hypotheses" -> (Some Discharge, Logical)
       | IDENT "Variables" -> (Some Discharge, Definitional)
       | IDENT "Axioms" -> (None, Logical)
-      | IDENT "Parameters" -> (None, Definitional) ] ]
+      | IDENT "Parameters" -> (None, Definitional)
+      | IDENT "Conjectures" -> (None, Conjectural) ] ]
   ;
   inline:
     [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index ac4e3b306..b4b6b8aab 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -271,7 +271,7 @@ and nf_atom env atom =
   | Aevar (ev,_) -> mkEvar ev
   | Aproj(p,c) ->
       let c = nf_accu env c in
-	mkProj(Projection.make p false,c)
+	mkProj(Projection.make p true,c)
   | _ -> fst (nf_atom_type env atom)
 
 and nf_atom_type env atom =
diff --git a/printing/printer.ml b/printing/printer.ml
index 141ae145d..652542825 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -559,8 +559,8 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
 	   ++ emacs_print_dependent_evars sigma seeds)
 	else
 	  let pei = pr_evars_int sigma 1 exl in
-	  (str "No more subgoals but non-instantiated existential " ++
-	   str "variables:" ++ fnl () ++ (hov 0 pei)
+	  (str "No more subgoals, but there are non-instantiated existential variables:"
+	   ++ fnl () ++ (hov 0 pei)
 	   ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
            str "You can use Grab Existential Variables.")
       end
@@ -625,17 +625,17 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
           begin match bgoals,shelf,given_up with
 	  | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals
           | [] , [] , _ ->
-	     msg_info (str "No more goals, however there are goals you gave up. You need to go back and solve them.");
+	     msg_info (str "No more subgoals, but there are some goals you gave up:");
 	     fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up
+            ++ fnl () ++ str "You need to go back and solve them."
           | [] , _ , _ ->
 	    msg_info (str "All the remaining goals are on the shelf.");
 	    fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
 	  | _ , _, _ ->
             let end_cmd =
-              strbrk "This subproof is complete, but there are still \
-              unfocused goals." ++
+              str "This subproof is complete, but there are some unfocused goals." ++
 	      (match Proof_global.Bullet.suggest p
               with None  -> str"" | Some s -> fnl () ++ str s) ++
               fnl ()
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3e2c813e3..8677b854d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -74,7 +74,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -665,4 +665,7 @@ let freeze ~marshallable =
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()
 let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof
+let copy_terminators ~src ~tgt =
+  assert(List.length src = List.length tgt);
+  List.map2 (fun op p -> { p with terminator = op.terminator }) src tgt
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 9d5038a3f..88e047782 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -66,7 +66,7 @@ type proof_object = {
 }
 
 type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry
+  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
   | Proved of Vernacexpr.opacity_flag *
              (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
               proof_object
@@ -197,3 +197,4 @@ type state
 val freeze : marshallable:[`Yes | `No | `Shallow] -> state
 val unfreeze : state -> unit
 val proof_of_state : state -> Proof.proof
+val copy_terminators : src:state -> tgt:state -> state
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 5eebd0d9d..c766f3fab 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -328,7 +328,7 @@ let check_exist =
 
 let standard_proof_terminator compute_guard hook =
   let open Proof_global in function
-  | Admitted (id,k,pe) ->
+  | Admitted (id,k,pe,_) ->
       admit (id,k,pe) hook ();
       Pp.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
@@ -347,8 +347,8 @@ let standard_proof_terminator compute_guard hook =
 
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in function
-  | Admitted (id,k,pe) ->
-      admit (id,k,pe) (hook None) ();
+  | Admitted (id,k,pe,ctx) ->
+      admit (id,k,pe) (hook (Some ctx)) ();
       Pp.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff, exports = match opaque with
@@ -480,14 +480,13 @@ let save_proof ?proof = function
               error "Admitted requires an explicit statement";
             let typ = Option.get const_entry_type in
             let ctx = Evd.evar_context_universe_context universes in
-            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None))
+            Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
         | None ->
             let id, k, typ = Pfedit.current_proof_statement () in
-            let ctx =
-              let evd, _ = Pfedit.get_current_goal_context () in
-              Evd.universe_context evd in
             (* This will warn if the proof is complete *)
-            let pproofs,_ = Proof_global.return_proof ~allow_partial:true () in
+            let pproofs, universes =
+              Proof_global.return_proof ~allow_partial:true () in
+            let ctx = Evd.evar_context_universe_context universes in
             let sec_vars =
               match  Pfedit.get_used_variables(), pproofs with
               | Some _ as x, _ -> x
@@ -497,7 +496,7 @@ let save_proof ?proof = function
                   let ids_def = Environ.global_vars_set env pproof in
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
-            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None))
+            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),universes)
       in
       Proof_global.get_terminator() pe
   | Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/stm/stm.ml b/stm/stm.ml
index fa3ffc7c6..373fd0ba3 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -671,11 +671,22 @@ end = struct (* {{{ *)
   let assign id what =
     if VCS.get_state id <> None then () else
     try match what with
-    | `Full s -> VCS.set_state id s
+    | `Full s ->
+         let s =
+           try
+            let prev = (VCS.visit id).next in
+            if is_cached prev
+            then { s with proof = 
+              Proof_global.copy_terminators
+                ~src:(get_cached prev).proof ~tgt:s.proof }
+            else s
+           with VCS.Expired -> s in
+         VCS.set_state id s
     | `Proof(ontop,(pstate,counters)) ->
          if is_cached ontop then
            let s = get_cached ontop in
-           let s = { s with proof = pstate } in
+           let s = { s with proof =
+             Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
            let s = { s with system =
              States.replace_summary s.system
                (Summary.surgery_summary
@@ -1119,7 +1130,7 @@ end = struct (* {{{ *)
         when is_tac expr && State.same_env o n -> (* A pure tactic *)
           Some (id, `Proof (prev, State.proof_part_of_frozen n))
       | Some _, Some s ->
-          msg_warning (str "Sending back a fat state");
+          msg_warning (str "STM: sending back a fat state");
           Some (id, `Full s)
       | _, Some s -> Some (id, `Full s) in
     let rec aux seen = function
@@ -2328,9 +2339,9 @@ let edit_at id =
     VCS.branch ~root:brinfo.VCS.root ~pos:brinfo.VCS.pos
       (Option.default brname bn)
       (no_edit brinfo.VCS.kind);
-      VCS.print ();
     VCS.delete_cluster_of id;
     VCS.gc ();
+    VCS.print ();
     Reach.known_state ~cache:(interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
@@ -2368,7 +2379,8 @@ let edit_at id =
           end else begin
             anomaly(str"Cannot leave an `Edit branch open")
           end
-      | false, None, _ -> backto id None
+      | false, None, Some(_,bn) -> backto id (Some bn)
+      | false, None, None -> backto id None
     in
     VCS.print ();
     rc
diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v
new file mode 100644
index 000000000..4f29b76c6
--- /dev/null
+++ b/test-suite/bugs/closed/3446.v
@@ -0,0 +1,47 @@
+(* 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). *)
+
+(* 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. *)
+
+
+(* 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 _ _). *)
+
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+Arguments projT1 {_ _} _.
+Notation "( x ; y )" := (existT _ x y).
+Notation pr1 := projT1.
+Notation "x .1" := (projT1 x) (at level 3).
+Notation "x .2" := (projT2 x) (at level 3).
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Notation "g 'o' f" := (compose g f) (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Arguments idpath {A a} , [A] a.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).
+Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3).
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT P) (pq : {p : u.1 = v.1 &  p # u.2 = v.2}), u = v.
+Instance isequiv_pr1_contr {A} {P : A -> Type} : IsEquiv (@pr1 A P) | 100.
+Admitted.
+
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT P) : u.1 = v.1 -> u = v := 
+  path_sigma_uncurried P u v o pr1^-1.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4057.v b/test-suite/bugs/closed/4057.v
new file mode 100644
index 000000000..4f0e696c9
--- /dev/null
+++ b/test-suite/bugs/closed/4057.v
@@ -0,0 +1,210 @@
+Require Coq.Strings.String.
+
+Set Implicit Arguments.
+
+Axiom falso : False.
+Ltac admit := destruct falso.
+
+Reserved Notation "[ x ]".
+
+Record string_like (CharType : Type) :=
+  {
+    String :> Type;
+    Singleton : CharType -> String where "[ x ]" := (Singleton x);
+    Empty : String;
+    Concat : String -> String -> String where "x ++ y" := (Concat x y);
+    bool_eq : String -> String -> bool;
+    bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y;
+    Length : String -> nat
+  }.
+
+Delimit Scope string_like_scope with string_like.
+Bind Scope string_like_scope with String.
+Arguments Length {_%type_scope _} _%string_like.
+Infix "++" := (@Concat _ _) : string_like_scope.
+
+Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String)
+  := Length s1 < Length s2 \/ s1 = s2.
+Infix "≤s" := str_le (at level 70, right associativity).
+
+Module Export ContextFreeGrammar.
+  Import Coq.Strings.String.
+  Import Coq.Lists.List.
+
+  Section cfg.
+    Variable CharType : Type.
+
+    Section definitions.
+
+      Inductive item :=
+    | NonTerminal (name : string).
+
+      Definition production := list item.
+      Definition productions := list production.
+
+      Record grammar :=
+        {
+          Start_symbol :> string;
+          Lookup :> string -> productions
+        }.
+    End definitions.
+
+    Section parse.
+      Variable String : string_like CharType.
+      Variable G : grammar.
+
+      Inductive parse_of : String -> productions -> Type :=
+      | ParseHead : forall str pat pats, parse_of_production str pat
+                                         -> parse_of str (pat::pats)
+      | ParseTail : forall str pat pats, parse_of str pats
+                                         -> parse_of str (pat::pats)
+      with parse_of_production : String -> production -> Type :=
+      | ParseProductionCons : forall str pat strs pats,
+                                parse_of_item str pat
+                                -> parse_of_production strs pats
+                                -> parse_of_production (str ++ strs) (pat::pats)
+      with parse_of_item : String -> item -> Type :=
+      | ParseNonTerminal : forall name str, parse_of str (Lookup G name)
+                                            -> parse_of_item str (NonTerminal 
+name).
+    End parse.
+  End cfg.
+
+End ContextFreeGrammar.
+Module Export ContextFreeGrammarProperties.
+
+  Section cfg.
+    Context CharType (String : string_like CharType) (G : grammar)
+            (P : String.string -> Type).
+
+    Fixpoint Forall_parse_of {str pats} (p : parse_of String G str pats)
+      := match p with
+           | @ParseHead _ _ _ str pat pats p'
+             => Forall_parse_of_production p'
+           | @ParseTail _ _ _ _ _ _ p'
+             => Forall_parse_of p'
+         end
+    with Forall_parse_of_production {str pat} (p : parse_of_production String G 
+str pat)
+         := let Forall_parse_of_item {str it} (p : parse_of_item String G str 
+it)
+                := match p return Type with
+                     | @ParseNonTerminal _ _ _ name str p'
+                       => (P name * Forall_parse_of p')%type
+                   end in
+            match p return Type with
+              | @ParseProductionCons _ _ _ str pat strs pats p' p''
+                => (Forall_parse_of_item p' * Forall_parse_of_production 
+p'')%type
+            end.
+
+    Definition Forall_parse_of_item {str it} (p : parse_of_item String G str it)
+      := match p return Type with
+           | @ParseNonTerminal _ _ _ name str p'
+             => (P name * Forall_parse_of p')%type
+         end.
+  End cfg.
+
+End ContextFreeGrammarProperties.
+
+Module Export DependentlyTyped.
+  Import Coq.Strings.String.
+
+  Section recursive_descent_parser.
+
+    Class parser_computational_predataT :=
+      { nonterminal_names_listT : Type;
+        initial_nonterminal_names_data : nonterminal_names_listT;
+        is_valid_nonterminal_name : nonterminal_names_listT -> string -> bool;
+        remove_nonterminal_name : nonterminal_names_listT -> string -> 
+nonterminal_names_listT }.
+
+  End recursive_descent_parser.
+
+End DependentlyTyped.
+Import Coq.Strings.String.
+Import Coq.Lists.List.
+
+Section cfg.
+  Context CharType (String : string_like CharType) (G : grammar).
+  Context (names_listT : Type)
+          (initial_names_data : names_listT)
+          (is_valid_name : names_listT -> string -> bool)
+          (remove_name : names_listT -> string -> names_listT).
+
+  Inductive minimal_parse_of
+  : forall (str0 : String) (valid : names_listT)
+           (str : String),
+      productions -> Type :=
+  | MinParseHead : forall str0 valid str pat pats,
+                     @minimal_parse_of_production str0 valid str pat
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  | MinParseTail : forall str0 valid str pat pats,
+                     @minimal_parse_of str0 valid str pats
+                     -> @minimal_parse_of str0 valid str (pat::pats)
+  with minimal_parse_of_production
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           production -> Type :=
+  | MinParseProductionNil : forall str0 valid,
+                              @minimal_parse_of_production str0 valid (Empty _) 
+nil
+  | MinParseProductionCons : forall str0 valid str strs pat pats,
+                               str ++ strs ≤s str0
+                               -> @minimal_parse_of_item str0 valid str pat
+                               -> @minimal_parse_of_production str0 valid strs 
+pats
+                               -> @minimal_parse_of_production str0 valid (str 
+++ strs) (pat::pats)
+  with minimal_parse_of_item
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           item -> Type :=
+  | MinParseNonTerminal
+    : forall str0 valid str name,
+        @minimal_parse_of_name str0 valid str name
+        -> @minimal_parse_of_item str0 valid str (NonTerminal name)
+  with minimal_parse_of_name
+       : forall (str0 : String) (valid : names_listT)
+                (str : String),
+           string -> Type :=
+  | MinParseNonTerminalStrLt
+    : forall str0 valid name str,
+        @minimal_parse_of str initial_names_data str (Lookup G name)
+        -> @minimal_parse_of_name str0 valid str name
+  | MinParseNonTerminalStrEq
+    : forall str valid name,
+        @minimal_parse_of str (remove_name valid name) str (Lookup G name)
+        -> @minimal_parse_of_name str valid str name.
+  Definition parse_of_item_name__of__minimal_parse_of_name
+  : forall {str0 valid str name} (p : @minimal_parse_of_name str0 valid str 
+name),
+      parse_of_item String G str (NonTerminal name).
+  Proof.
+    admit.
+  Defined.
+
+End cfg.
+
+Section recursive_descent_parser.
+  Context (CharType : Type)
+          (String : string_like CharType)
+          (G : grammar).
+  Context {premethods : parser_computational_predataT}.
+  Let P : string -> Prop.
+  Proof.
+    admit.
+  Defined.
+
+  Let mp_parse_nonterminal_name str0 valid str nonterminal_name
+    := { p' : minimal_parse_of_name String G initial_nonterminal_names_data 
+remove_nonterminal_name str0 valid str nonterminal_name & Forall_parse_of_item 
+P (parse_of_item_name__of__minimal_parse_of_name p') }.
+
+  Goal False.
+  Proof.
+    clear -mp_parse_nonterminal_name.
+    subst P.
+    simpl in *.
+    admit.
+  Qed.
diff --git a/test-suite/ide/bug4246.fake b/test-suite/ide/bug4246.fake
new file mode 100644
index 000000000..16b552f67
--- /dev/null
+++ b/test-suite/ide/bug4246.fake
@@ -0,0 +1,14 @@
+# first proof
+ADD { Lemma a : True. }
+ADD { Proof using. }
+ADD here { trivial. } # first error
+ADD { fail. }
+ADD { Qed. }
+WAIT
+EDIT_AT here
+# Fixing the proof
+ADD { Qed. }
+WAIT
+EDIT_AT here
+ADD { Qed. }
+JOIN
diff --git a/test-suite/ide/bug4249.fake b/test-suite/ide/bug4249.fake
new file mode 100644
index 000000000..20afe0fb8
--- /dev/null
+++ b/test-suite/ide/bug4249.fake
@@ -0,0 +1,16 @@
+ADD { Lemma a : True. }
+ADD here { Proof using. }
+ADD { fail. }
+ADD { trivial. } # first error
+ADD { Qed. }
+WAIT
+EDIT_AT here
+# Fixing the proof
+ADD fix { trivial. }
+ADD { Qed. }
+WAIT
+EDIT_AT fix
+ADD { Qed. }
+EDIT_AT fix
+ADD { Qed. }
+JOIN
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 0cf8d7337..c1d958b9d 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -41,7 +41,7 @@ Ltac do_nat n tac :=
 (** Do something on the last hypothesis, or fail *)
 
 Ltac on_last_hyp tac :=
-  match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end.
+  lazymatch goal with [ H : _ |- _ ] => tac H end.
 
 (** Destructs one pair, without care regarding naming. *)
 
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index d7a292f4c..a9a7251c5 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -90,7 +90,7 @@ module Parser = struct (* {{{ *)
       in find ~-1 0
     else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s))
 
-  let eat_blanks s = snd (eat_rex "[ \n\t]*") s
+  let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s
 
   let s = ref ""