Merge branch 'v8.5'

12 files changed, 91 insertions, 92 deletions

diff --git a/Makefile.build b/Makefile.build
index d9ad1942f7..018937fc6d 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -525,6 +525,7 @@ hightactics: tactics/hightactics.cma
 .PHONY: init theories theories-light
 .PHONY: logic arith bool narith zarith qarith lists strings sets
 .PHONY: fsets relations wellfounded reals setoids sorting numbers noreal
+.PHONY: msets mmaps
 
 init: $(INITVO)
 
@@ -552,6 +553,8 @@ classes: $(CLASSESVO)
 program: $(PROGRAMVO)
 structures: $(STRUCTURESVO)
 vectors: $(VECTORSVO)
+msets: $(MSETSVO)
+mmaps: $(MMAPSVO)
 
 noreal: unicode logic arith bool zarith qarith lists sets fsets \
 	relations wellfounded setoids sorting
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index e1a6bc7c1d..f02f03dcb1 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -269,7 +269,7 @@ type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
   | LocalNotConstructor
-  | LocalNonPar of int * int
+  | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
 
@@ -291,9 +291,9 @@ let explain_ind_err ntyp env0 nbpar c err =
     | LocalNotConstructor ->
 	raise (InductiveError
 		 (NotConstructor (env,c',Rel (ntyp+nbpar))))
-    | LocalNonPar (n,l) ->
+    | LocalNonPar (n,i,l) ->
 	raise (InductiveError
-		 (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar))))
+		 (NonPar (env,c',n,Rel i,Rel (l+nbpar))))
 
 let failwith_non_pos n ntypes c =
   for k = n to n + ntypes - 1 do
@@ -323,7 +323,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     | _::hyps ->
         match whd_betadeltaiota env lpar.(k) with
 	  | Rel w when w = index -> check (k-1) (index+1) hyps
-	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
+	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
   in check (nparams-1) (n-nhyps) hyps;
   if not (Array.for_all (noccur_between n ntypes) largs') then
     failwith_non_pos_vect n ntypes largs'
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 940b5528d3..891d95378b 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -207,7 +207,8 @@ let rec pp_instr i =
 	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
 	     str " bodies = " ++
 	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
-  | Kgetglobal (id,_u) -> str "getglobal " ++ pr_con id
+  | Kgetglobal (id,u) ->
+    str "getglobal " ++ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
   | Kconst sc ->
       str "const " ++ pp_struct_const sc
   | Kmakeblock(n, m) ->
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 3c137ee92b..e3457006d0 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -344,7 +344,7 @@ type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
   | LocalNotConstructor
-  | LocalNonPar of int * int
+  | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
 
@@ -365,9 +365,9 @@ let explain_ind_err id ntyp env nbpar c nargs err =
     | LocalNotConstructor ->
 	raise (InductiveError
 		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs)))
-    | LocalNonPar (n,l) ->
+    | LocalNonPar (n,i,l) ->
 	raise (InductiveError
-		 (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar))))
+		 (NonPar (env,c',n,mkRel i, mkRel (l+nbpar))))
 
 let failwith_non_pos n ntypes c =
   for k = n to n + ntypes - 1 do
@@ -396,7 +396,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     | _::hyps ->
         match kind_of_term (whd_betadeltaiota env lpar.(k)) with
 	  | Rel w when Int.equal w index -> check (k-1) (index+1) hyps
-	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
+	  | _ -> raise (IllFormedInd (LocalNonPar (k+1, index, l)))
   in check (nparams-1) (n-nhyps) hyps;
   if not (Array.for_all (noccur_between n ntypes) largs') then
     failwith_non_pos_vect n ntypes largs'
diff --git a/library/library.ml b/library/library.ml
index 45fce1c26c..f7ca4e9760 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -379,7 +379,7 @@ let access_table what tables dp i =
     | Fetched t -> t
     | ToFetch f ->
       let dir_path = Names.DirPath.to_string dp in
-      msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
+      Flags.if_verbose msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
       let t =
         try fetch_delayed f
         with Faulty f ->
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
index 979a1cdc41..244eb85fc2 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -11,11 +11,12 @@ Require Import EqNat.
 
 Extract Inlined Constant Nat.add => "(Prelude.+)".
 Extract Inlined Constant Nat.mul => "(Prelude.*)".
-Extract Inlined Constant Nat.div => "Prelude.div".
 Extract Inlined Constant Nat.max => "Prelude.max".
 Extract Inlined Constant Nat.min => "Prelude.min".
 Extract Inlined Constant Init.Nat.add => "(Prelude.+)".
 Extract Inlined Constant Init.Nat.mul => "(Prelude.*)".
+Extract Inlined Constant Init.Nat.max => "Prelude.max".
+Extract Inlined Constant Init.Nat.min => "Prelude.min".
 Extract Inlined Constant Compare_dec.lt_dec => "(Prelude.<)".
 Extract Inlined Constant Compare_dec.leb => "(Prelude.<=)".
 Extract Inlined Constant Compare_dec.le_lt_dec => "(Prelude.<=)".
@@ -23,5 +24,12 @@ Extract Inlined Constant EqNat.beq_nat => "(Prelude.==)".
 Extract Inlined Constant EqNat.eq_nat_decide => "(Prelude.==)".
 Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".
 
-Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
-Extract Constant minus => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+Extract Constant Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+Extract Constant Init.Nat.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
+Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
+
+Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
\ No newline at end of file
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v
index 3f645db9b1..cbbfda75e5 100644
--- a/plugins/extraction/ExtrHaskellZNum.v
+++ b/plugins/extraction/ExtrHaskellZNum.v
@@ -12,8 +12,10 @@ Require Import EqNat.
 Extract Inlined Constant Z.add => "(Prelude.+)".
 Extract Inlined Constant Z.sub => "(Prelude.-)".
 Extract Inlined Constant Z.mul => "(Prelude.*)".
-Extract Inlined Constant Z.div => "Prelude.div".
 Extract Inlined Constant Z.max => "Prelude.max".
 Extract Inlined Constant Z.min => "Prelude.min".
 Extract Inlined Constant Z_ge_lt_dec => "(Prelude.>=)".
 Extract Inlined Constant Z_gt_le_dec => "(Prelude.>)".
+
+Extract Constant Z.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
+Extract Constant Z.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/stm/stm.ml b/stm/stm.ml
index bf91c3aa4f..e6271f6089 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1773,7 +1773,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), cache, true
       | `Cmd { cast = x; cqueue = `QueryQueue cancel }
         when Flags.async_proofs_is_master () -> (fun () ->
-            reach ~cache:`Shallow view.next;
+            reach view.next;
             Query.vernac_interp cancel view.next id x
           ), cache, false
       | `Cmd { cast = x } -> (fun () ->
@@ -1935,7 +1935,7 @@ let finish ?(print_goals=false) () =
   VCS.print ();
   (* Some commands may by side effect change the proof mode *)
   match VCS.get_branch head with
-  | { VCS.kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode
+  | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode
   | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode
   | _ -> ()
 
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 08df91507e..23f33081b4 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -2,11 +2,6 @@ Axioms:
 foo : nat
 Axioms:
 foo : nat
-Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZAdd
-Fetching opaque proofs from disk for Coq.Arith.PeanoNat
-Fetching opaque proofs from disk for Coq.Classes.Morphisms
-Fetching opaque proofs from disk for Coq.Init.Logic
-Fetching opaque proofs from disk for Coq.Numbers.NatInt.NZBase
 Axioms:
 extensionality : forall (P Q : Type) (f g : P -> Q),
                  (forall x : P, f x = g x) -> f = g
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index e902370c35..4b92d57082 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -386,12 +386,12 @@ let implicit () =
     print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
     print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
     print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n";
-    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let mlpack_rules () =
     print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
     print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
     print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n";
-    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+    print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
 in
   let v_rules () =
     print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ac8ca3a11d..7a3bcfba80 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1086,7 +1086,7 @@ let error_bad_ind_parameters env c n v1 v2  =
   let pv1 = pr_lconstr_env env Evd.empty v1 in
   let pv2 = pr_lconstr_env env Evd.empty v2 in
   str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
-  str " as " ++ pr_nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "."
+  str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "."
 
 let error_same_names_types id =
   str "The name" ++ spc () ++ pr_id id ++ spc () ++
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 9df5a411ba..11857b5724 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -613,7 +613,12 @@ let shrink_body c =
       else mkLambda (n,t,b), succ i, mkRel i :: args)
      (b, 1, []) ctx
   in List.map (fun (c,t) -> (c,None,t)) ctx, b', Array.of_list args
-      
+
+let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
+
+let add_hint local prg cst =
+  Hints.add_hints local [Id.to_string prg.prg_name] (unfold_entry cst)
+
 let declare_obligation prg obl body ty uctx =
   let body = prg.prg_reduce body in
   let ty = Option.map prg.prg_reduce ty in
@@ -640,9 +645,7 @@ let declare_obligation prg obl body ty uctx =
       let constant = Declare.declare_constant obl.obl_name ~local:true
 	(DefinitionEntry ce,IsProof Property)
       in
-	if not opaque then
-	  Hints.add_hints false [Id.to_string prg.prg_name]
-	    (Hints.HintsUnfoldEntry [EvalConstRef constant]);
+	if not opaque then add_hint false prg constant;
 	definition_message obl.obl_name;
 	{ obl with obl_body = 
 	    if poly then 
@@ -774,7 +777,7 @@ let not_transp_msg =
   str "Obligation should be transparent but was declared opaque." ++ spc () ++
     str"Use 'Defined' instead."
 
-let error_not_transp () = pperror not_transp_msg
+let err_not_transp () = pperror not_transp_msg
 
 let rec string_of_list sep f = function
     [] -> ""
@@ -797,74 +800,61 @@ let solve_by_tac name evi t poly ctx =
   Inductiveops.control_only_guard (Global.env ()) (fst body);
   (fst body), entry.Entries.const_entry_type, ctx'
 
+let obligation_hook prg obl num auto ctx' _ gr =
+  let obls, rem = prg.prg_obligations in
+  let cst = match gr with ConstRef cst -> cst | _ -> assert false in
+  let transparent = evaluable_constant cst (Global.env ()) in
+  let () = match obl.obl_status with
+  | Evar_kinds.Expand -> if not transparent then err_not_transp ()
+  | Evar_kinds.Define op -> if not op && not transparent then err_not_transp ()
+  in
+  let obl = { obl with obl_body = Some (DefinedObl cst) } in
+  let () = if transparent then add_hint true prg cst in
+  let obls = Array.copy obls in
+  let _ = obls.(num) <- obl in
+  let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
+  let ctx' =
+    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
+      (* This context is already declared globally, we cannot
+          instantiate the rigid variables anymore *)
+      Evd.abstract_undefined_variables ctx'
+    else ctx'
+  in
+  let prg = { prg with prg_ctx = ctx' } in
+  let () =
+    try ignore (update_obls prg obls (pred rem))
+    with e when Errors.noncritical e ->
+      let e = Errors.push e in
+      pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
+  in
+  if pred rem > 0 then begin
+    let deps = dependencies obls num in
+    if not (Int.Set.is_empty deps) then
+      ignore (auto (Some prg.prg_name) None deps)
+  end
+
 let rec solve_obligation prg num tac =
   let user_num = succ num in
   let obls, rem = prg.prg_obligations in
   let obl = obls.(num) in
+  let remaining = deps_remaining obls obl.obl_deps in
+  let () =
     if not (Option.is_empty obl.obl_body) then
-      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
-    else
-      match deps_remaining obls obl.obl_deps with
-      | [] ->
-          let obl = subst_deps_obl obls obl in
-          let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
-            let evd = Evd.from_env ~ctx:prg.prg_ctx Environ.empty_env in
-            Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type
-              (fun ctx' -> Lemmas.mk_hook (fun strength gr ->
-		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
-		let obl =
-		  let transparent = evaluable_constant cst (Global.env ()) in
-		  let body =
-		    match obl.obl_status with
-		    | Evar_kinds.Expand ->
-			if not transparent then error_not_transp ()
-			else DefinedObl cst
-		    | Evar_kinds.Define opaque ->
-			if not opaque && not transparent then error_not_transp ()
-			else DefinedObl cst
-		  in
-		    if transparent then
-		      Hints.add_hints true [Id.to_string prg.prg_name]
-			(Hints.HintsUnfoldEntry [EvalConstRef cst]);
-		    { obl with obl_body = Some body }
-		in
-		let obls = Array.copy obls in
-		let _ = obls.(num) <- obl in
-		let ctx' = 
-		  let ctx = 
-		    match ctx' with
-		    | None -> prg.prg_ctx
-		    | Some ctx' -> ctx'
-		  in
-  		    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
-		      (* This context is already declared globally, we cannot 
-			 instantiate the rigid variables anymore *) 
-		      Evd.abstract_undefined_variables ctx
-		    else ctx
-		in
-		let res = 
-		  try update_obls 
-			{prg with prg_body = prg.prg_body;
-			  prg_type = prg.prg_type;
-			  prg_ctx = ctx' }
-			  
-			obls (pred rem)
-		  with e when Errors.noncritical e ->
-                    let e = Errors.push e in
-                    pperror (Errors.iprint (Cerrors.process_vernac_interp_error e))
-		in
-		  match res with
-		  | Remain n when n > 0 ->
-		      let deps = dependencies obls num in
-			if not (Int.Set.is_empty deps) then
-			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
-		  | _ -> ()));
-	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
-		     Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type);
-	    ignore (Pfedit.by (snd (get_default_tactic ())));
-	    Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
-      | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
-		      ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))
+      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.");
+    if not (List.is_empty remaining) then
+      pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
+        ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
+  in
+  let obl = subst_deps_obl obls obl in
+  let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in
+  let evd = Evd.from_env ~ctx:prg.prg_ctx Environ.empty_env in
+  let auto n tac oblset = auto_solve_obligations n ~oblset tac in
+  let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
+  let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type hook in
+  let () = trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
+            Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
+  let _ = Pfedit.by (snd (get_default_tactic ())) in
+  Option.iter (fun tac -> Pfedit.set_end_tac tac) tac
 
 and obligation (user_num, name, typ) tac =
   let num = pred user_num in