From 76d6a8cfb0448ade98e1a7abc92ff1bf5075fe8f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 22 Aug 2015 18:05:59 +0200
Subject: Code cleaning in Obligations.

This commit is chiefly about moving code around to ease readability.
---
 toplevel/obligations.ml | 126 ++++++++++++++++++++++--------------------------
 1 file changed, 58 insertions(+), 68 deletions(-)

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
-- 
cgit v1.2.3


From ae8f843303060e1db96f72b42d744b8b200b0968 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 1 Sep 2015 12:49:52 +0200
Subject: STM: save a full state for queries.

In PIDE based UIs queries can be delegated too, hence to speed up
things I was saving a shallow state.  Unfortunately a shallow state
breaks section/modules commands, and a query can be the last entry
of a section/module.  (A shallow state does essentially drop the libstack).

The easy solution is to save a complete state.
A better one would be to refine the static analysis of the document and
decide which kind of saved state one needs.
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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
   | _ -> ()
 
-- 
cgit v1.2.3


From 0f2d41755d99770c4576776462a4e433fb8f0a02 Mon Sep 17 00:00:00 2001
From: mlasson
Date: Thu, 25 Jun 2015 15:41:27 +0200
Subject: Missing argument "-c" for coqdep in coq_makefile

Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d
were generated by a call to coqdep using the argument -c (for ocaml
code). While doing some finetuning of the generation of implicit rules,
this commit removed (I think by mistake) this "-c". And without this
-c argument coqdep output nothing on mllib files leading to incorrect
linking of mllibs.
---
 tools/coq_makefile.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 71134c2d97..934a632dd1 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";
-- 
cgit v1.2.3


From 518049fe7f689489842fdfa670f57b618f125f31 Mon Sep 17 00:00:00 2001
From: mlasson
Date: Thu, 25 Jun 2015 16:40:24 +0200
Subject: Add an if_verbose for "Fetching opaque proofs ..."

I do not think that this information is worth displaying without
the verbose flag.
---
 library/library.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 ->
-- 
cgit v1.2.3


From 60b5e9c05e0c168e30eafede545c221e63d12ea2 Mon Sep 17 00:00:00 2001
From: mlasson
Date: Thu, 25 Jun 2015 19:50:15 +0200
Subject: Also there's an extra space in the error message.

---
 toplevel/himsg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 () ++
-- 
cgit v1.2.3


From b06d3badbf5a8aa95e5150c2dc0b3fd44e1269ab Mon Sep 17 00:00:00 2001
From: mlasson
Date: Wed, 15 Jul 2015 16:19:01 +0200
Subject: Implementing Herbelin's fix for the "NonPar" bug

Hugo Herbelin proposed to modify directly the function
"check_correct_par" to simplify commit c12b430
(see the pullrequest's discussion).

Note that the constructor "LocalNonPar" has now three arguments (instead
of two). In LocalNonPar (n,i,l) n denotes the position among real
arguments (ie. ignoring letins), i is the rel index of the expecting argument
in the context of parameters and l is the index of the inductive.
---
 checker/indtypes.ml | 8 ++++----
 kernel/indtypes.ml  | 8 ++++----
 2 files changed, 8 insertions(+), 8 deletions(-)

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/indtypes.ml b/kernel/indtypes.ml
index 9c79009dba..8c89abe940 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -339,7 +339,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
 
@@ -360,9 +360,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
@@ -391,7 +391,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'
-- 
cgit v1.2.3


From c7fd3cb7945bcd385ace06f583d1b57681c8716d Mon Sep 17 00:00:00 2001
From: Nickolai Zeldovich
Date: Thu, 16 Jul 2015 18:24:19 -0400
Subject: Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.v

The previous extraction of [Nat.div] for Haskell did not properly handle
divide-by-zero.  Fix it by introducing an explicit [if] statement in the
generated Haskell code.

Also, introduce a similar extraction rule for [Nat.modulo], with the same
check for modulo-by-zero.
---
 plugins/extraction/ExtrHaskellNatNum.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
index 979a1cdc41..81d76a5ffa 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -11,7 +11,6 @@ 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.+)".
@@ -23,5 +22,8 @@ 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 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)".
-- 
cgit v1.2.3


From 5c060d56a9d94d74cdeca6f6b424306218e81562 Mon Sep 17 00:00:00 2001
From: Nickolai Zeldovich
Date: Thu, 16 Jul 2015 18:31:00 -0400
Subject: Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.v

The previous extraction of [Z.div] for Haskell did not properly handle
divide-by-zero.  Fix it by introducing an explicit [if] statement in the
generated Haskell code.

Also, introduce a similar extraction rule for [Z.modulo], with the same
check for modulo-by-zero.
---
 plugins/extraction/ExtrHaskellZNum.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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)".
-- 
cgit v1.2.3


From b5c646a37ac0375f9fbb2427549c925ee3f127ad Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 3 Sep 2015 19:37:22 +0200
Subject: Improve directives for Haskell extraction of nat.

---
 plugins/extraction/ExtrHaskellNatNum.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
index 81d76a5ffa..244eb85fc2 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -15,6 +15,8 @@ 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.<=)".
@@ -24,6 +26,10 @@ Extract Inlined Constant Peano_dec.eq_nat_dec => "(Prelude.==)".
 
 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
-- 
cgit v1.2.3


From 6000ddffed48b804669a5eae9be7c536bf5e19c5 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Wed, 2 Sep 2015 18:50:09 -0700
Subject: print universes when dumping bytecode.

---
 kernel/cbytecodes.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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) ->
-- 
cgit v1.2.3


From 26be4ca94f8ba0a03826a2df09491bb0d96d7363 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 3 Sep 2015 20:50:31 +0200
Subject: Update test-suite after 518049fe7.

"Fetching opaque proofs" notices are not printed by default anymore.
---
 test-suite/output/PrintAssumptions.out | 5 -----
 1 file changed, 5 deletions(-)

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
-- 
cgit v1.2.3


From 5080991902a05ee720ab1d6fa1c9d592d3ffd36c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Sep 2015 13:20:32 +0200
Subject: Adding a Makefile target for the MSets and MMaps directories.

The target creation process should eventually be automated, because it
is tedious and error-prone as witnessed by this commit.
---
 Makefile.build | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Makefile.build b/Makefile.build
index 83cdd506e3..6ceff2de95 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -524,6 +524,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)
 
@@ -551,6 +552,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
-- 
cgit v1.2.3