From 498d22e9575ecf2515ae592a07b3f50e7648882f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 18 Jan 2015 23:49:38 +0100
Subject: Fix a big bug in native_compute tactic: since Hugo's 364decf59c, it
 was actually calling the VM at Qed time.

---
 proofs/redexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 1858886731..1383d75567 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -234,7 +234,7 @@ let reduction_of_red_expr env =
 	 with Not_found ->
 	   error("unknown user-defined reduction \""^s^"\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
-  | CbvNative o -> (contextualize cbv_native cbv_native o, VMcast)
+  | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
   in
     reduction_of_red_expr
 
-- 
cgit v1.2.3


From bef0d3bc629e25a281b4ed2424dc3b8405349acf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Jan 2015 17:39:05 +0100
Subject: Making unification of LetIn's expressions more consistent (see
 #3920).

Unifying two let-in's expresions syntactically is a heuristic
(compared to performing the zeta-reduction). This heuristic was
requiring unification of types which is too strong for the heuristic
to work uniformly since the types might only be related modulo
subtyping.

The patch is to remove the unification of types, which allows then to
have the heuristic work uniformly on the bodies. On the other side, I
hope it does not loose (still heuristical) unifications compared to
before (presumably, since instantiating the evars in the body will
induce constraints for solving potential evars in the types of the
let-in bodies, but this would need a proof). Anyway, it is not about
correction, it is about a heuristic, which maybe done too early
actually.
---
 pretyping/evarconv.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index a95af2532f..616ceeabdc 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -555,8 +555,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
         | LetIn (na,b1,t1,c'1), LetIn (_,b2,t2,c'2) ->
         let f1 i =
           ise_and i
-	    [(fun i -> evar_conv_x ts env i CONV t1 t2);
-	     (fun i -> evar_conv_x ts env i CONV b1 b2);
+	    [(fun i -> evar_conv_x ts env i CONV b1 b2);
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
-- 
cgit v1.2.3


From 35fde66d67a7a4e36f04adc53347bbb87a34356e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 20 Jan 2015 15:02:48 +0100
Subject: Fix a critical bug in machine arithmetic for native compiler.

---
 kernel/nativevalues.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index d7a2195052..e4a7799933 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -370,6 +370,11 @@ type coq_pair =
   | Paccu of t
   | PPair of t * t
 
+type coq_zn2z =
+  | Zaccu of t
+  | ZW0
+  | ZWW of t * t
+
 let mkCarry b i =
   if b then (Obj.magic (C1(of_uint i)):t)
   else (Obj.magic (C0(of_uint i)):t)
@@ -413,8 +418,13 @@ let subcarryc accu x y =
 let of_pair (x, y) =
   (Obj.magic (PPair(of_uint x, of_uint y)):t)
 
+let zn2z_of_pair (x,y) =
+  if Uint31.equal x (Uint31.of_uint 0) &&
+    Uint31.equal y (Uint31.of_uint 0) then Obj.magic ZW0
+  else (Obj.magic (ZWW(of_uint x, of_uint y)) : t)
+
 let no_check_mulc x y =
-    of_pair(Uint31.mulc (to_uint x) (to_uint y))
+  zn2z_of_pair(Uint31.mulc (to_uint x) (to_uint y))
 
 let mulc accu x y =
   if is_int x && is_int y then no_check_mulc x y
-- 
cgit v1.2.3


From fb860f9ea8dca5395ca9f2f350a68c1760c84ce4 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 21 Jan 2015 08:41:38 +0100
Subject: Reference manual: fix typo in doc of [tryif/then/else].

Fixes #3939.---
 doc/refman/RefMan-ltac.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index b90e682df1..de8c26943c 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -474,7 +474,7 @@ $v_2$). Branching is left-associative.
 
 The tactic
 \begin{quote}
-{\tt if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$}
+{\tt tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$}
 \end{quote}
 is a generalization of the biased-branching tactics above. The
 expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied
@@ -482,7 +482,7 @@ to each subgoal independently. For each goal where $v_1$ succeeds at
 least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied
 collectively to the generated subgoals. The $v_2$ tactic can trigger
 backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt
-  if {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is
+  tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is
 equivalent to $v_1;v_2$. In each of the goals where $v_1$ does not
 succeed at least once, {\tacexpr}$_3$ is evaluated in $v_3$ which is
 is then applied to the goal.
-- 
cgit v1.2.3


From 2e1ab34a9feaa3fac6220400acbc7c710b0a0211 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 21 Jan 2015 09:05:36 +0100
Subject: Reference manual: pass over the credit section for English.

---
 doc/refman/RefMan-pre.tex | 41 +++++++++++++++++++++--------------------
 1 file changed, 21 insertions(+), 20 deletions(-)

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index e75ade9419..4af5c8fc65 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -939,9 +939,9 @@ projects:
 \begin{itemize}
 \item A new asynchronous evaluation and compilation mode by Enrico
   Tassi with help from Bruno Barras and Carst Tankink.
-\item The full integration of the new proof engine by Arnaud Spiwack
+\item Full integration of the new proof engine by Arnaud Spiwack
   helped by Pierre-Marie Pédrot,
-\item The addition of conversion and reduction based on native compilation
+\item Addition of conversion and reduction based on native compilation
   by Maxime Dénès and Benjamin Grégoire.
 \item Full universe polymorphism for definitions and inductive types by
   Matthieu Sozeau.
@@ -958,20 +958,21 @@ The way Coq processes a document in batch and interactive mode has
 been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
 proofs, the text between Proof and Qed, can be processed
 asynchronously, decoupling the checking of definitions and statements
-from the checking of proofs.  In interactive use, this improves the
-reactiveness of the system, since proofs can be processed in the
-background.  Similarly the compilation of a file can be split into two
-phases:  the first one checking only definitions and statements and
-the second one checking proofs.  A file resulting from the first
-phase, .vio extension, can be already Required.  All .vio files can be
-turned into complete .vo files in parallel.  The same infrastructure
-also allows terminating tactics to be run in parallel on a set of
-goals via the \verb=par:= goal selector.
-
-CoqIDE was modified to cope with asynchronous checking of the document.
-Its source code was also made separate from the one of Coq making it no
-more a special user interface and allowing its release cycle to be
-decoupled with the one of Coq.
+from the checking of proofs.  It improves the responsiveness of
+interactive development, since proofs can be processed in the
+background.  Similarly compilation of a file can be split into two
+phases: the first one checking only definitions and statements and the
+second one checking proofs.  A file resulting from the first
+phase~--~with the .vio extension~--~can be already Required.  All .vio
+files can be turned into complete .vo files in parallel.  The same
+infrastructure also allows terminating tactics to be run in parallel
+on a set of goals via the \verb=par:= goal selector.
+
+CoqIDE was modified to cope with asynchronous checking of the
+document.  Its source code was also made separate from that of Coq, so
+that CoqIDE no longer has a special status among user interfaces,
+paving the way for decoupling its release cycle from that of Coq in
+the future.
 
 Carst Tankink developed a Coq back end for user interfaces built on
 Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
@@ -982,13 +983,13 @@ funded by the Paral-ITP French ANR project.
 The full universe polymorphism extension was designed by Matthieu
 Sozeau. It conservatively extends the universes system and core calculus
 with definitions and inductive declarations parameterized by universes
-and constraints. It is based on a change of the kernel architecture to
+and constraints. It is based on a modification of the kernel architecture to
 handle constraint checking only, leaving the generation of constraints
 to the refinement/type inference engine. Accordingly, tactics are now
 fully universe aware, resulting in more localized error messages in case
 of inconsistencies and allowing higher-level algorithms like unification
 to be entirely type safe. The internal representation of universes has
-been modified but this invisible to the user. 
+been modified but this is invisible to the user. 
 
 The underlying logic has been extended with $\eta$-conversion for
 records defined with primitive projections by Matthieu Sozeau. This
@@ -999,11 +1000,11 @@ with typed equality. Primitive projections, which do not carry the
 parameters of the record and are rigid names (not defined as a
 pattern-matching construct), make working with nested records more
 manageable in terms of time and space consumption. This extension and
-universe polymorphism were carried partly while the author was working
+universe polymorphism were carried out partly while Matthieu Sozeau was working
 at the IAS in Princeton.
 
 The guard condition has been made compliant with extensional equality
-principles such as propositional equality and univalence, thanks to
+principles such as propositional extensionality and univalence, thanks to
 Maxime Dénès and Bruno Barras. To ensure compatibility with the
 univalence axiom, a new flag ``-indices-matter'' has been implemented, 
 taking into account the universe levels of indices when computing the
-- 
cgit v1.2.3


From 9e7e259e9f81eefd505b04e5e17b06136055e1ee Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 21 Jan 2015 09:07:10 +0100
Subject: Reference Manual/Credits: remove a duplicate.

---
 doc/refman/RefMan-pre.tex | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 4af5c8fc65..cf6dae34c3 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1023,9 +1023,7 @@ and improvements regarding the different components of the system.
 
 Maxime Dénès and Benjamin Grégoire developed an implementation of the
 conversion test using the OCaml native compiler.
-Bruno Barras and Maxime Dénès fixed a problem in the guard condition
-leading to a refutation of standard axioms like propositional
-extensionality or univalence.
+
 Maxime Dénès maintained the bytecode-based reduction machine.
 
 Pierre Courtieu contributed new features for using {\Coq} through Proof
-- 
cgit v1.2.3


From 5b653d2bb4d9f7b4c6f1faf4b3c17d6400cadf48 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 21 Jan 2015 09:44:24 +0100
Subject: Reference manual/Credits: populate the "various smaller-scale
 improvements" part.

---
 doc/refman/RefMan-pre.tex | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index cf6dae34c3..e160022279 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1014,21 +1014,29 @@ the relations between homotopy theory and type theory.
 {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes
 and improvements regarding the different components of the system.
 
-% High-Level Specification Language: 
-% - tactics in terms
-% - Universe inconsistency and unification error messages
-% - Named existentials
-
-% Opam Coq Guillaume Claret and Thomas Braibant 
-
 Maxime Dénès and Benjamin Grégoire developed an implementation of the
 conversion test using the OCaml native compiler.
 
 Maxime Dénès maintained the bytecode-based reduction machine.
 
+Pierre-Marie Pédrot has extended the syntax of terms to,
+experimentally, allow holes in terms to be solved by a locally
+specified tactic.
+
+Existential variables are referred to by identifiers rather than mere
+numbers, thanks to Hugo Herbelin.
+
+Error messages for universe inconsistencies have been improved by
+Matthieu Sozeau. Error messages for unification and type inference
+failures have been improved by Hugo Herbelin, Pierre-Marie Pédrot and
+Arnaud Spiwack.
+
 Pierre Courtieu contributed new features for using {\Coq} through Proof
 General and for better interactive experience (bullets, Search etc).
 
+A distribution channel for Coq packages using the Opam tool has been
+developed by Thomas Braibant and Guillaume Claret.
+
 \begin{flushright}
 Paris, January 2015\\
 Hugo Herbelin \& Matthieu Sozeau\\
-- 
cgit v1.2.3


From b855224b5ce5deda9853af1bed9b135a7ea9a76b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 21 Jan 2015 10:01:49 +0100
Subject: Reference Manual/Credits: native compute is a major contribution.

It is, at the very least, listed as such in the overview. So, I moved it to the relevant part and expanded the description with a sentence or two.---
 doc/refman/RefMan-pre.tex | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index e160022279..66f3369e3b 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1011,12 +1011,14 @@ taking into account the universe levels of indices when computing the
 levels of inductive types. This supports using Coq as a tool to explore
 the relations between homotopy theory and type theory.
 
+Maxime Dénès and Benjamin Grégoire developed an implementation of
+conversion test and normal form computation using the OCaml native
+compiler. It complements the virtual machine conversion offering much
+faster computation for expensive functions.
+
 {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes
 and improvements regarding the different components of the system.
 
-Maxime Dénès and Benjamin Grégoire developed an implementation of the
-conversion test using the OCaml native compiler.
-
 Maxime Dénès maintained the bytecode-based reduction machine.
 
 Pierre-Marie Pédrot has extended the syntax of terms to,
-- 
cgit v1.2.3


From 3527a32a9c055a1438f0c85b77d3dbd8d38cbd32 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 21 Jan 2015 10:36:37 +0100
Subject: Reference Manual/Credits: expand the paragraph on the new proof
 engine to match the overall style.

---
 doc/refman/RefMan-pre.tex | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 66f3369e3b..f45072ca43 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -950,9 +950,18 @@ projects:
   Matthieu Sozeau.
 \end{itemize}
 
-The full integration of the proof engine brings to primitive tactics and
-the user level Ltac language deep tactic backtracking and multi-goal
-handling.
+The full integration of the proof engine, by Arnaud Spiwack and
+Pierre-Marie Pédrot, brings to primitive tactics and the user level
+Ltac language dependent subgoals, deep backtracking and multiple goal
+handling, along with miscellaneous features and an improved potential
+for future modifications. Dependent subgoals allow statements in a
+goal to mention the proof of another. Proofs of unsolved subgoals
+appear as existential variables. Primitive backtracking make it
+possible to write a tactic with several possible outcomes which are
+tried successively when subsequent tactics fail. Primitives are also
+available to control the backtracking behavior of tactics. Multiple
+goal handling paves the way for smarter automation tactics. It is
+currently used for simple goal manipulation such as goal reordering.
 
 The way Coq processes a document in batch and interactive mode has
 been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
-- 
cgit v1.2.3


From feca7916eaaceea96be4c15f08895578b3703a1c Mon Sep 17 00:00:00 2001
From: mlasson
Date: Wed, 21 Jan 2015 11:07:32 +0100
Subject: Add the possibility of defining opaque terms with program.

---
 toplevel/command.ml      |  4 ++--
 toplevel/command.mli     |  2 +-
 toplevel/obligations.ml  | 22 +++++++++++++---------
 toplevel/obligations.mli |  6 +++---
 4 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9cb3bb8660..608747d0e4 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -746,8 +746,8 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
-  let ce = definition_entry ~types:t ~poly ~univs:ctx ~eff def in
+let declare_fix ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
+  let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
   declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref := declare_fix
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 894333ad53..1de47d38c4 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -167,5 +167,5 @@ val do_cofixpoint :
 
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : definition_kind -> Univ.universe_context -> Id.t ->
+val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
   Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index aa0685861a..456a6f9d0f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -21,7 +21,7 @@ open Pp
 open Errors
 open Util
 
-let declare_fix_ref = ref (fun _ _ _ _ _ _ -> assert false)
+let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
 
 let trace s =
@@ -319,6 +319,7 @@ type program_info = {
   prg_kind : definition_kind;
   prg_reduce : constr -> constr;
   prg_hook : unit Lemmas.declaration_hook;
+  prg_opaque : bool;
 }
 
 let assumption_message = Declare.assumption_message
@@ -512,8 +513,9 @@ let declare_definition prg =
   let body, typ = subst_body true prg in
   let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
     (Evd.evar_universe_context_subst prg.prg_ctx) in
+  let opaque = prg.prg_opaque in
   let ce =
-    definition_entry ~types:(nf typ) ~poly:(pi2 prg.prg_kind) 
+    definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
       ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
     progmap_remove prg;
@@ -564,6 +566,7 @@ let declare_mutual_definition l =
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
   let (local,poly,kind) = first.prg_kind in
   let fixnames = first.prg_deps in
+  let opaque = first.prg_opaque in
   let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
   let indexes, fixdecls =
     match fixkind with
@@ -584,7 +587,7 @@ let declare_mutual_definition l =
   in
   (* Declare the recursive definitions *)
   let ctx = Evd.evar_context_universe_context first.prg_ctx in
-  let kns = List.map4 (!declare_fix_ref (local, poly, kind) ctx) 
+  let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
@@ -640,7 +643,7 @@ let declare_obligation prg obl body ty uctx =
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
 
-let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook =
   let obls', b = 
     match b with
     | None ->
@@ -664,7 +667,8 @@ let init_prog_info n b t ctx deps fixkind notations obls impls kind reduce hook
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
-      prg_hook = hook; }
+      prg_hook = hook;
+      prg_opaque = opaque; }
 
 let get_prog name =
   let prg_infos = !from_prg in
@@ -976,9 +980,9 @@ let show_term n =
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
 let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
-    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) obls =
+    ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls =
   let info = str (Id.to_string n) ++ str " has type-checked" in
-  let prg = init_prog_info n term t ctx [] None [] obls implicits kind reduce hook in
+  let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose msg_info (info ++ str ".");
@@ -994,11 +998,11 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
-    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) notations fixkind =
+    ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info n (Some b) t ctx deps (Some fixkind) 
+     let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
      in progmap_add n prg) l;
     let _defined =
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 582b493548..d39e18a480 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -17,7 +17,7 @@ open Decl_kinds
 open Tacexpr
 
 (** Forward declaration. *)
-val declare_fix_ref : (definition_kind -> Univ.universe_context -> Id.t ->
+val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
   Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref
 
 val declare_definition_ref :
@@ -69,7 +69,7 @@ val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook -> obligation_info -> progress
+  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -85,7 +85,7 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->
-  ?hook:unit Lemmas.declaration_hook ->
+  ?hook:unit Lemmas.declaration_hook -> ?opaque:bool ->
   notations ->
   fixpoint_kind -> unit
 
-- 
cgit v1.2.3


From 4f632721be8b083126f49dd900a3294521879ec4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 23 Jan 2015 14:15:10 +0100
Subject: Extraction: fix #3629.

The control flow of extraction is hard to read due to exceptions. When meeting
an inlined constant extracted to custom code, they could desynchronize some
tables in charge of detecting name clashes, leading to an anomaly.
---
 plugins/extraction/ocaml.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 30ac3d3f89..ce88ea6d29 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -634,7 +634,10 @@ and pp_module_type params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (mp, sign) ->
       push_visible mp params;
-      let l = List.map pp_specif sign in
+      let try_pp_specif x l =
+	try pp_specif x :: l with Failure "empty phrase" -> l
+      in
+      let l = List.fold_right try_pp_specif sign [] in
       pop_visible ();
       str "sig " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -707,7 +710,10 @@ and pp_module_expr params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MEstruct (mp, sel) ->
       push_visible mp params;
-      let l = List.map pp_structure_elem sel in
+      let try_pp_structure_elem x l =
+	try pp_structure_elem x :: l with Failure "empty phrase" -> l
+      in
+      let l = List.fold_right try_pp_structure_elem sel [] in
       pop_visible ();
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
-- 
cgit v1.2.3