From f1a8b27ffe0df4f207b0cfaac067c8201d07ae16 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 Nov 2015 14:41:14 +0100
Subject: Hashconsing modules.

Modules inserted into the environment were not hashconsed, leading to an
important redundancy, especially in module signatures that are always fully
expanded.

This patch divides by two the size and memory consumption of module-heavy
files by hashconsing modules before putting them in the environment. Note
that this is not a real hashconsing, in the sense that we only hashcons the
inner terms contained in the modules, that are only mapped over. Compilation
time should globally decrease, even though some files definining a lot of
modules may see their compilation time increase.

Some remaining overhead may persist, as for instance module inclusion is not
hashconsed.
---
 kernel/declareops.ml  | 85 +++++++++++++++++++++++++++++++++++++++++++++++++++
 kernel/declareops.mli |  1 +
 kernel/names.mli      |  2 ++
 kernel/safe_typing.ml |  2 ++
 4 files changed, 90 insertions(+)

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d9bd5c445e..f8b5981fa0 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -308,3 +308,88 @@ let string_of_side_effect { Entries.eff } = match eff with
   | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")"
   | Entries.SEscheme (cl,_) ->
       "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")"
+
+(** Hashconsing of modules *)
+
+let hcons_functorize hty he hself f = match f with
+| NoFunctor e ->
+  let e' = he e in
+  if e == e' then f else NoFunctor e'
+| MoreFunctor (mid, ty, nf) ->
+  (** FIXME *)
+  let mid' = mid in
+  let ty' = hty ty in
+  let nf' = hself nf in
+  if mid == mid' && ty == ty' && nf == nf' then f
+  else MoreFunctor (mid, ty', nf')
+
+let hcons_module_alg_expr me = me
+
+let rec hcons_structure_field_body sb = match sb with
+| SFBconst cb ->
+  let cb' = hcons_const_body cb in
+  if cb == cb' then sb else SFBconst cb'
+| SFBmind mib ->
+  let mib' = hcons_mind mib in
+  if mib == mib' then sb else SFBmind mib'
+| SFBmodule mb ->
+  let mb' = hcons_module_body mb in
+  if mb == mb' then sb else SFBmodule mb'
+| SFBmodtype mb ->
+  let mb' = hcons_module_body mb in
+  if mb == mb' then sb else SFBmodtype mb'
+
+and hcons_structure_body sb =
+  (** FIXME *)
+  let map (l, sfb as fb) =
+    let l' = Names.Label.hcons l in
+    let sfb' = hcons_structure_field_body sfb in
+    if l == l' && sfb == sfb' then fb else (l', sfb')
+  in
+  List.smartmap map sb
+
+and hcons_module_signature ms =
+  hcons_functorize hcons_module_body hcons_structure_body hcons_module_signature ms
+
+and hcons_module_expression me =
+  hcons_functorize hcons_module_body hcons_module_alg_expr hcons_module_expression me
+
+and hcons_module_implementation mip = match mip with
+| Abstract -> Abstract
+| Algebraic me ->
+  let me' = hcons_module_expression me in
+  if me == me' then mip else Algebraic me'
+| Struct ms ->
+  let ms' = hcons_module_signature ms in
+  if ms == ms' then mip else Struct ms
+| FullStruct -> FullStruct
+
+and hcons_module_body mb =
+  let mp' = mb.mod_mp in
+  let expr' = hcons_module_implementation mb.mod_expr in
+  let type' = hcons_module_signature mb.mod_type in
+  let type_alg' = mb.mod_type_alg in
+  let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in
+  let delta' = mb.mod_delta in
+  let retroknowledge' = mb.mod_retroknowledge in
+
+  if
+    mb.mod_mp == mp' &&
+    mb.mod_expr == expr' &&
+    mb.mod_type == type' &&
+    mb.mod_type_alg == type_alg' &&
+    mb.mod_constraints == constraints' &&
+    mb.mod_delta == delta' &&
+    mb.mod_retroknowledge == retroknowledge'
+  then mb
+  else {
+    mod_mp = mp';
+    mod_expr = expr';
+    mod_type = type';
+    mod_type_alg = type_alg';
+    mod_constraints = constraints';
+    mod_delta = delta';
+    mod_retroknowledge = retroknowledge';
+  }
+
+and hcons_module_type_body mtb = hcons_module_body mtb
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 86ba29b8b7..ad2b5d0a6c 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -77,3 +77,4 @@ val inductive_context : mutual_inductive_body -> universe_context
 
 val hcons_const_body : constant_body -> constant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
+val hcons_module_body : module_body -> module_body
diff --git a/kernel/names.mli b/kernel/names.mli
index 72dff03be7..1e79f4dde4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -160,6 +160,8 @@ sig
   module Set : Set.S with type elt = t
   module Map : Map.ExtS with type key = t and module Set := Set
 
+  val hcons : t -> t
+
 end
 
 (** {6 Unique names for bound modules} *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0926d35f6d..62753962c8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -561,6 +561,7 @@ let add_mind dir l mie senv =
 let add_modtype l params_mte inl senv =
   let mp = MPdot(senv.modpath, l) in
   let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte  in
+  let mtb = Declareops.hcons_module_body mtb in
   let senv' = add_field (l,SFBmodtype mtb) MT senv in
   mp, senv'
 
@@ -581,6 +582,7 @@ let full_add_module_type mp mt senv =
 let add_module l me inl senv =
   let mp = MPdot(senv.modpath, l) in
   let mb = Mod_typing.translate_module senv.env mp inl me in
+  let mb = Declareops.hcons_module_body mb in
   let senv' = add_field (l,SFBmodule mb) M senv in
   let senv'' =
     if Modops.is_functor mb.mod_type then senv'
-- 
cgit v1.2.3


From 4341f37cf3c51ed82c23f05846c8e6e8823d3cd6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 10 Mar 2016 19:02:16 +0100
Subject: Primitive projections: protect kernel from erroneous definitions.

E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.

- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
  must be strictly non recursive for BiFinite declarations).
---
 kernel/closure.ml                  |  2 +-
 kernel/indtypes.ml                 | 19 ++++++++++++-------
 pretyping/evarconv.ml              |  2 +-
 printing/prettyp.ml                |  4 ++--
 test-suite/success/primitiveproj.v | 16 +---------------
 5 files changed, 17 insertions(+), 26 deletions(-)

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 2ba80d8362..93e63d0fb5 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -784,7 +784,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (_,projs,pbs)) when
-	mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
+	mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 49e8583158..acf5ab17d3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -452,7 +452,7 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
 
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
-let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
+let check_positivity_one recursive (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
   let lparams = rel_context_length hyps in
   let nmr = rel_context_nhyps hyps in
   (* Checking the (strict) positivity of a constructor argument type [c] *)
@@ -538,6 +538,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 
           | Prod (na,b,d) ->
 	      let () = assert (List.is_empty largs) in
+	      if not recursive && not (noccur_between n ntypes b) then
+	        raise (InductiveError BadEntry);
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
                 check_constr_rec ienv' nmr' (recarg::lrec) d
@@ -570,9 +572,11 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
   and nmr' = array_min nmr irecargs_nmr
   in (nmr', mk_paths (Mrec ind) irecargs)
 
-let check_positivity kn env_ar params inds =
+let check_positivity kn env_ar params finite inds =
   let ntypes = Array.length inds in
-  let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
+  let recursive = finite != Decl_kinds.BiFinite in
+  let rc = Array.mapi (fun j t -> (Mrec (kn,j),t))
+		      (Rtree.mk_rec_calls ntypes) in
   let lra_ind = Array.rev_to_list rc in
   let lparams = rel_context_length params in
   let nmr = rel_context_nhyps params in
@@ -581,7 +585,7 @@ let check_positivity kn env_ar params inds =
       List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
     let nargs = rel_context_nhyps sign - nmr in
-    check_positivity_one ienv params (kn,i) nargs lcnames lc
+    check_positivity_one recursive ienv params (kn,i) nargs lcnames lc
   in
   let irecargs_nmr = Array.mapi check_one inds in
   let irecargs = Array.map snd irecargs_nmr
@@ -807,10 +811,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map2 build_one_packet inds recargs in
-  let pkt = packets.(0) in	  
+  let pkt = packets.(0) in
   let isrecord = 
     match isrecord with
-    | Some (Some rid) when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1
+    | Some (Some rid) when pkt.mind_kelim == all_sorts
+			   && Array.length pkt.mind_consnames == 1
 			   && pkt.mind_consnrealargs.(0) > 0 ->
       (** The elimination criterion ensures that all projections can be defined. *)
       let u = 
@@ -851,7 +856,7 @@ let check_inductive env kn mie =
   (* First type-check the inductive definition *)
   let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let (nmr,recargs) = check_positivity kn env_ar_par params inds in
+  let (nmr,recargs) = check_positivity kn env_ar_par params mie.mind_entry_finite inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 637a9e50e0..690b974be5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -854,7 +854,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
+    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite -> 
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index fd51fd6b0f..4d9d40ae08 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -215,8 +215,8 @@ let print_polymorphism ref =
 let print_primitive_record recflag mipv = function
   | Some (Some (_, ps,_)) ->
     let eta = match recflag with
-    | Decl_kinds.CoFinite -> mt ()
-    | Decl_kinds.Finite | Decl_kinds.BiFinite -> str " and has eta conversion"
+    | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
+    | Decl_kinds.BiFinite -> str " and has eta conversion"
     in
     [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
   | _ -> []
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 281d707cb3..b5e6ccd618 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -35,10 +35,6 @@ Set Implicit Arguments.
 
 Check nat.
 
-(* Inductive X (U:Type) := Foo (k : nat) (x : X U).  *)
-(* Parameter x : X nat. *)
-(* Check x.(k). *)
-
 Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }.
 
 Parameter x:X nat.
@@ -49,18 +45,8 @@ Inductive Y := { next : option Y }.
 
 Check _.(next) : option Y.
 Lemma eta_ind (y : Y) : y = Build_Y y.(next).
-Proof. reflexivity. Defined.
-
-Variable t : Y.
-
-Fixpoint yn (n : nat) (y : Y) : Y := 
-  match n with
-    | 0 => t
-    | S n => {| next := Some (yn n y) |}
-  end.
+Proof. Fail reflexivity. Abort.
 
-Lemma eta_ind'  (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
-Proof. reflexivity. Defined.
 
 
 (* 
-- 
cgit v1.2.3


From e9bf68016ce9e04feb63222ff4bbafd27531f564 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 11 Mar 2016 10:32:14 +0100
Subject: According to Bruno, my fix for #4588 seems to be enough.

So adding a test-suite file and closing the bug.
---
 test-suite/bugs/closed/4588.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/bugs/closed/4588.v

diff --git a/test-suite/bugs/closed/4588.v b/test-suite/bugs/closed/4588.v
new file mode 100644
index 0000000000..ff66277e03
--- /dev/null
+++ b/test-suite/bugs/closed/4588.v
@@ -0,0 +1,10 @@
+Set Primitive Projections.
+
+(* This proof was accepted in Coq 8.5 because the subterm specs were not
+projected correctly *)
+Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }.
+
+Fail Fixpoint loop (x : foo) : False :=
+  loop (proj2 x _ x).
+
+Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)).
-- 
cgit v1.2.3


From e171456870f9893d582d53114d4f87e634c007e5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 14 Mar 2016 14:24:33 +0100
Subject: Trying to circumvent hdiutil error 5341 by padding.

When generating the OS X Coq + CoqIDE bundle, hdiutil often produces error
5341. This seems to be a known bug on Apple's side, occurring for some sizes of
dmg files. We try to change the current (problematic) size by adding a file
full of random bits.
---
 dev/make-macos-dmg.sh | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/dev/make-macos-dmg.sh b/dev/make-macos-dmg.sh
index 20b7b5b531..b43ada9076 100755
--- a/dev/make-macos-dmg.sh
+++ b/dev/make-macos-dmg.sh
@@ -28,4 +28,8 @@ codesign -f -s - $APP
 mkdir -p $DMGDIR
 ln -sf /Applications $DMGDIR/Applications
 cp -r $APP $DMGDIR
+
+# Temporary countermeasure to hdiutil error 5341
+head -c9703424 /dev/urandom > $DMGDIR/.padding
+
 hdiutil create -imagekey zlib-level=9 -volname CoqIDE_$VERSION -srcfolder $DMGDIR -ov -format UDZO CoqIDE_$VERSION.dmg
-- 
cgit v1.2.3


From 779fd5d9a4982b19fd257b61f444ae8e6155dcbe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Mar 2016 19:50:29 +0100
Subject: Fix bug when a sort is ascribed to a Record

Forcefully equating it to the inferred level is not always desirable or possible.
---
 test-suite/success/univers.v | 17 +++++++++++++++++
 toplevel/record.ml           | 13 +++++++------
 2 files changed, 24 insertions(+), 6 deletions(-)

diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index e00701fb68..269359ae62 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,3 +60,20 @@ Qed.
 (* Submitted by Danko Ilik (bug report #1507); related to LetIn *)
 
 Record U : Type := { A:=Type; a:A }.
+
+(** Check assignement of sorts to inductives and records. *)
+
+Variable sh : list nat.
+
+Definition is_box_in_shape (b :nat * nat) := True.
+Definition myType := Type.
+
+Module Ind.
+Inductive box_in : myType :=
+  myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in.
+End Ind.
+
+Module Rec.
+Record box_in : myType :=
+  BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }.
+End Rec.
\ No newline at end of file
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 04da628c33..200d1a9387 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -140,12 +140,13 @@ let typecheck_params_and_fields def id pl t ps nots fs =
 	arity, evars
       else
 	let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in
-	  if Univ.is_small_univ univ then
-	    (* We can assume that the level aritysort is not constrained
-  	       and clear it. *)
-	    mkArity (ctx, Sorts.sort_of_univ univ),
-	    Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
-	  else arity, evars
+	if Univ.is_small_univ univ &&
+	   Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then
+	   (* We can assume that the level in aritysort is not constrained
+	       and clear it, if it is flexible *)
+	  mkArity (ctx, Sorts.sort_of_univ univ),
+	  Evd.set_eq_sort env_ar evars (Prop Pos) aritysort
+	else arity, evars
   in
   let evars, nf = Evarutil.nf_evars_and_universes evars in
   let newps = map_rel_context nf newps in
-- 
cgit v1.2.3


From 8f5ca2a6100eb243d2a9842a13e02b793ee0aea1 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 14 Mar 2016 11:13:21 +0100
Subject: Try eta-expansion of records only on non-recursive ones

---
 pretyping/unification.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 31fd711bf9..9b6e856b80 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -609,7 +609,7 @@ let is_eta_constructor_app env ts f l1 term =
   | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite &&
+      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Decl_kinds.BiFinite &&
           Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
 	(** Check that the other term is neutral *)
 	is_neutral env ts term
-- 
cgit v1.2.3


From 45e43916a7ce756b617b7ba3f8062f7956872fb3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Mar 2016 17:10:16 +0100
Subject: Tentative fix for bug #4614: "Fully check the document" is
 uninterruptable.

The SIGINT sent to the master coqtop process was lost in a watchdog thread,
so that the STM resulted in an inconsistent state. This patch catches gracefully
the exception and kills the task as if it were normally cancelled. Note that
it probably won't work on non-POSIX architectures, but it does not really
matter because interrupt was already badly handled anyway.
---
 stm/asyncTaskQueue.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 5f018ec39d..8649a14c54 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -184,6 +184,13 @@ module Make(T : Task) = struct
         let () = Unix.sleep 1 in
         kill_if ()
     in
+    let kill_if () =
+      try kill_if ()
+      with Sys.Break ->
+        let () = stop_waiting := true in
+        let () = TQueue.broadcast queue in
+        Worker.kill proc
+    in
     let _ = Thread.create kill_if () in
 
     try while true do
-- 
cgit v1.2.3


From e5b40d615d0ed9819f6ac8345ed924d8a501172e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Mar 2016 19:47:49 +0100
Subject: CoqIDE is more resilient to initialization errors.

We force the STM to finish after the initialization request so as to raise
exceptions that may have been generated by the initialization process. Likewise,
we simply die when the initialization request fails in CoqIDE instead of just
printing an error message.

This is the fix for the underlying issue of bug #4591, but it does not solve
the bug yet.
---
 ide/coqOps.ml    | 5 ++++-
 ide/ide_slave.ml | 1 +
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 58f5eda62e..850b41e596 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -864,7 +864,10 @@ object(self)
   method initialize =
     let get_initial_state =
       let next = function
-      | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return ()
+      | Fail (_, _, message) ->
+        let message = "Couldn't initialize coqtop\n\n" ^ message in
+        let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok ~message_type:`ERROR ~message () in
+        ignore (popup#run ()); exit 1
       | Good id -> initial_state <- id; Coq.return () in
       Coq.bind (Coq.init (get_filename ())) next in
     Coq.seq get_initial_state Coq.PrintOpt.enforce
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bd98fe16e3..2e6a361c66 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -361,6 +361,7 @@ let init =
                0 (Printf.sprintf "Add LoadPath \"%s\". " dir)
            else Stm.get_current_state (), `NewTip in
          Stm.set_compilation_hints file;
+         Stm.finish ();
          initial_id
    end
 
-- 
cgit v1.2.3


From 34c467a4e41e20a9bf1318d47fbc09da94c5ad97 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Mar 2016 19:56:52 +0100
Subject: Fix #4591: Uncaught exception in directory browsing.

We protect Sys.readdir calls againts any nasty exception.
---
 lib/system.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/lib/system.ml b/lib/system.ml
index 0ad43a7423..36fdf26089 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -26,6 +26,8 @@ let ok_dirname f =
   not (String.List.mem f !skipped_dirnames) &&
   (match Unicode.ident_refutation f with None -> true | _ -> false)
 
+let readdir dir = try Sys.readdir dir with any -> [||]
+
 let all_subdirs ~unix_path:root =
   let l = ref [] in
   let add f rel = l := (f, rel) :: !l in
@@ -38,7 +40,7 @@ let all_subdirs ~unix_path:root =
 	  add file newrel;
 	  traverse file newrel
         end)
-      (Sys.readdir dir)
+      (readdir dir)
   in
   if exists_dir root then traverse root [];
   List.rev !l
@@ -58,7 +60,7 @@ let dirmap = ref StrMap.empty
 
 let make_dir_table dir =
   let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
-  Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
+  Array.fold_left filter_dotfiles StrSet.empty (readdir dir)
 
 let exists_in_dir_respecting_case dir bf =
   let contents, cached =
-- 
cgit v1.2.3