Merge branch 'v8.5'

29 files changed, 362 insertions, 211 deletions

diff --git a/CHANGES b/CHANGES
index a279e487e..2cc91bbd6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,14 +12,15 @@ Program
 - The "Shrink Obligations" flag now applies to all obligations, not only those
   solved by the automatic tactic.
 
-Changes from V8.5beta3
-======================
+Changes from V8.5beta3 to V8.5
+==============================
 
-Vernacular commands
-- Flag -compat 8.4 now loads Coq.Compat.Coq84. The standard way of putting Coq
-  in v8.4 compatibility mode is to pass the command line flag "-compat 8.4". It
-  can be followed by "-require Coq.Compat.AdmitAxiom" if 8.4 behavior of admit is
-  needed, in which case it uses an axiom.
+Tools
+
+- Flag "-compat 8.4" now loads Coq.Compat.Coq84. The standard way of
+  putting Coq in v8.4 compatibility mode is to pass the command line flag
+  "-compat 8.4". It can be followed by "-require Coq.Compat.AdmitAxiom"
+  if the 8.4 behavior of admit is needed, in which case it uses an axiom.
 
 Specification language
 
@@ -34,6 +35,10 @@ Tactics
 - Syntax "p/c" for on-the-fly application of a lemma c before
   introducing along pattern p changed to p%c1..%cn. The feature and
   syntax are in experimental stage.
+- "Proof using" does not clear unused section variables.
+- "refine" has been changed back to the 8.4 behavior of shelving subgoals
+  that occur in other subgoals. The "refine" tactic of 8.5beta2 has been
+  renamed "simple refine"; it does not shelve any subgoal.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index f45072ca4..e0dc49666 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -956,20 +956,20 @@ 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
+appear as existential variables. Primitive backtracking makes 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
+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.  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
+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
@@ -977,13 +977,13 @@ 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
+{\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
+Carst Tankink developed a {\Coq} back-end for user interfaces built on
 Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
 help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander
 Faithfull and Jesper Bengtson).  The development of such features was
@@ -1017,7 +1017,7 @@ 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
-levels of inductive types. This supports using Coq as a tool to explore
+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
@@ -1025,17 +1025,23 @@ 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.
+{\Coq} 8.5 also comes with a bunch of many various smaller-scale
+changes and improvements regarding the different components of the
+system. We shall only list a few of them.
+
+Pierre Boutillier developed an improved tactic for simplification of
+expressions called {\tt cbn}.
 
-Maxime Dénès maintained the bytecode-based reduction machine.
+Maxime Dénès maintained the bytecode-based reduction machine. Pierre
+Letouzey maintained the extraction mechanism.
 
 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.
+numbers, thanks to Hugo Herbelin who also improved the tactic language
+here and there.
 
 Error messages for universe inconsistencies have been improved by
 Matthieu Sozeau. Error messages for unification and type inference
@@ -1043,14 +1049,43 @@ 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.
+General and for better interactive experience (bullets, Search, etc).
+
+The efficiency of the whole system has been significantly improved
+thanks to contributions from Pierre-Marie Pédrot.
+
+A distribution channel for {\Coq} packages using the OPAM tool has
+been initiated by Thomas Braibant and developed by Guillaume Claret,
+with contributions by Enrico Tassi and feedback from Hugo Herbelin.
+
+Packaging tools were provided by Pierre Letouzey and Enrico Tassi
+(Windows), Pierre Boutillier, Matthieu Sozeau and Maxime Dénès (MacOS
+X). Maxime Dénès improved significantly the testing and benchmarking
+support.
+
+Many power users helped to improve the design of the new features via
+the bug tracker, the coq development mailing list or the coq-club
+mailing list. Special thanks are going to the users who contributed
+patches and intensive brain-storming, starting with Jason Gross,
+Jonathan Leivent, Greg Malecha, Clément Pit-Claudel, Marc Lasson,
+Lionel Rieg. It would however be impossible to mention with precision
+all names of people who to some extent influenced the development.
+
+Version 8.5 is one of the most important release of {\Coq}. Its
+development spanned over about 3 years and a half with about one year
+of beta-testing. General maintenance during part or whole of this
+period has been done by Pierre Boutillier, Pierre Courtieu, Maxime
+Dénès, Hugo Herbelin, Pierre Letouzey, Guillaume Melquiond,
+Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi as
+well as Bruno Barras, Yves Bertot, Frédéric Besson, Xavier Clerc,
+Pierre Corbineau, Jean-Christophe Filliâtre, Julien Forest, Sébastien
+Hinderer, Assia Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François
+Ripault, Carst Tankink. Maxime Dénès brilliantly coordinated the
+release process.
 
 \begin{flushright}
-Paris, January 2015\\
-Hugo Herbelin \& Matthieu Sozeau\\
+Paris, January 2015, revised December 2015,\\
+Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
 \end{flushright}
 
 
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 481afa8f8..ed1b79e56 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -186,7 +186,7 @@ in Section~\ref{ProofWith}.
 \subsubsection{{\tt Proof using} options}
 \optindex{Default Proof Using}
 \optindex{Suggest Proof Using}
-\optindex{Proof Using Clear Unused}
+% \optindex{Proof Using Clear Unused}
 
 The following options modify the behavior of {\tt Proof using}.
 
@@ -201,12 +201,12 @@ The following options modify the behavior of {\tt Proof using}.
   When {\tt Qed} is performed, suggest a {\tt using} annotation if
   the user did not provide one.
 
-\variant{\tt Unset Proof Using Clear Unused.}
-
-  When {\tt Proof using a} all section variables but for {\tt a} and
-  the variables used in the type of {\tt a} are cleared.
-  This option can be used to turn off this behavior.
-
+% \variant{\tt Unset Proof Using Clear Unused.}
+% 
+%   When {\tt Proof using a} all section variables but for {\tt a} and
+%   the variables used in the type of {\tt a} are cleared.
+%   This option can be used to turn off this behavior.
+% 
 \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
 \comindex{Collection}\label{Collection}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 34b974381..f268d8276 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -219,8 +219,10 @@ difference: the user can leave some holes (denoted by \texttt{\_} or
 {\tt (\_:\type)}) in the term. {\tt refine} will generate as
 many subgoals as there are holes in the term. The type of holes must be
 either synthesized by the system or declared by an
-explicit cast like \verb|(_:nat->Prop)|. This low-level
-tactic can be useful to advanced users.
+explicit cast like \verb|(_:nat->Prop)|. Any subgoal that occurs in other
+subgoals is automatically shelved, as if calling {\tt shelve\_unifiable}
+(see Section~\ref{shelve}).
+This low-level tactic can be useful to advanced users.
 
 \Example
 
@@ -256,6 +258,13 @@ Defined.
   which type cannot be inferred. Put a cast around it.
 \end{ErrMsgs}
 
+\begin{Variants}
+\item {\tt simple refine \term}\tacindex{simple refine}
+
+  This tactic behaves like {\tt refine}, but it does not shelve any
+  subgoal. It does not perform any beta-reduction either.
+\end{Variants}
+
 \subsection{\tt apply \term}
 \tacindex{apply}
 \label{apply}
@@ -4955,8 +4964,8 @@ back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
 \begin{Variants}
   \item \texttt{shelve\_unifiable}\tacindex{shelve\_unifiable}
 
-    Shelves only these goals under focused which are mentioned in other goals.
-    Goals which appear in the type of other goals can be solve by unification.
+    Shelves only the goals under focus that are mentioned in other goals.
+    Goals that appear in the type of other goals can be solved by unification.
 
 \Example
 \begin{coq_example}
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 97f856944..8cf3b8194 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -171,10 +171,7 @@ let push_vars ids (db,avoid) =
   let ids',avoid' = rename_vars avoid ids in
   ids', (ids' @ db, avoid')
 
-let get_db_name n (db,_) =
-  let id = List.nth db (pred n) in
-  if Id.equal id dummy_name then Id.of_string "__" else id
-
+let get_db_name n (db,_) = List.nth db (pred n)
 
 (*S Renamings of global objects. *)
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f4d14af62..2dc2420c4 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -201,36 +201,6 @@ let parse_ind_args si args relmax =
 	 | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
 
-let oib_equal o1 o2 =
-  Id.equal o1.mind_typename o2.mind_typename &&
-  List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
-    begin
-      match o1.mind_arity, o2.mind_arity with
-      | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} ->
-	eq_constr c1 c2 && Sorts.equal s1 s2
-      | TemplateArity p1, TemplateArity p2 ->
-	let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in
-	  List.equal eq p1.template_param_levels p2.template_param_levels &&
-	    Univ.Universe.equal p1.template_level p2.template_level
-      | _, _ -> false
-    end &&
-    Array.equal Id.equal o1.mind_consnames o2.mind_consnames
-
-let eq_record x y =
-  Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y
-
-let mib_equal m1 m2 =
-  Array.equal oib_equal m1.mind_packets m1.mind_packets &&
-  eq_record m1.mind_record m2.mind_record &&
-  (m1.mind_finite : Decl_kinds.recursivity_kind) == m2.mind_finite &&
-  Int.equal m1.mind_ntypes m2.mind_ntypes &&
-  List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
-  Int.equal m1.mind_nparams m2.mind_nparams &&
-  Int.equal m1.mind_nparams_rec m2.mind_nparams_rec &&
-  List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
-  (* Univ.UContext.eq *) m1.mind_universes == m2.mind_universes (** FIXME *)
-  (* m1.mind_universes = m2.mind_universes *)
-
 (*S Extraction of a type. *)
 
 (* [extract_type env db c args] is used to produce an ML type from the
@@ -360,14 +330,9 @@ and extract_type_scheme env db c p =
 
 and extract_ind env kn = (* kn is supposed to be in long form *)
   let mib = Environ.lookup_mind kn env in
-  try
-    (* For a same kn, we can get various bodies due to module substitutions.
-       We hence check that the mib has not changed from recording
-       time to retrieving time. Ideally we should also check the env. *)
-    let (mib0,ml_ind) = lookup_ind kn in
-    if not (mib_equal mib mib0) then raise Not_found;
-    ml_ind
-  with Not_found ->
+  match lookup_ind kn mib with
+  | Some ml_ind -> ml_ind
+  | None ->
     (* First, if this inductive is aliased via a Module,
        we process the original inductive if possible.
        When at toplevel of the monolithic case, we cannot do much
@@ -523,28 +488,25 @@ and extract_type_cons env db dbmap c i =
 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
 
 and mlt_env env r = match r with
+  | IndRef _ | ConstructRef _ | VarRef _ -> None
   | ConstRef kn ->
-      (try
-	 if not (visible_con kn) then raise Not_found;
-	 match lookup_term kn with
-	   | Dtype (_,vl,mlt) -> Some mlt
+     let cb = Environ.lookup_constant kn env in
+     match cb.const_body with
+     | Undef _ | OpaqueDef _ -> None
+     | Def l_body ->
+        match lookup_typedef kn cb with
+        | Some _ as o -> o
+        | None ->
+           let typ = Typeops.type_of_constant_type env cb.const_type
+           (* FIXME not sure if we should instantiate univs here *) in
+	   match flag_of_type env typ with
+	   | Info,TypeScheme ->
+	      let body = Mod_subst.force_constr l_body in
+	      let s = type_sign env typ in
+	      let db = db_from_sign s in
+	      let t = extract_type_scheme env db body (List.length s)
+	      in add_typedef kn cb t; Some t
 	   | _ -> None
-       with Not_found ->
-	 let cb = Environ.lookup_constant kn env in
-	 let typ = Typeops.type_of_constant_type env cb.const_type
- (* FIXME not sure if we should instantiate univs here *) in
-	 match cb.const_body with
-	   | Undef _ | OpaqueDef _ -> None
-	   | Def l_body ->
-	       (match flag_of_type env typ with
-		  | Info,TypeScheme ->
-		      let body = Mod_subst.force_constr l_body in
-		      let s,vl = type_sign_vl env typ in
-		      let db = db_from_sign s in
-		      let t = extract_type_scheme env db body (List.length s)
-		      in add_term kn (Dtype (r, vl, t)); Some t
-		  | _ -> None))
-  | _ -> None
 
 and expand env = type_expand (mlt_env env)
 and type2signature env = type_to_signature (mlt_env env)
@@ -555,16 +517,18 @@ let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env)
 (*s Extraction of the type of a constant. *)
 
 let record_constant_type env kn opt_typ =
-  try
-    if not (visible_con kn) then raise Not_found;
-    lookup_type kn
-  with Not_found ->
-    let typ = match opt_typ with
-      | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type
-      | Some typ -> typ
-    in let mlt = extract_type env [] 1 typ []
-    in let schema = (type_maxvar mlt, mlt)
-    in add_type kn schema; schema
+  let cb = lookup_constant kn env in
+  match lookup_cst_type kn cb with
+  | Some schema -> schema
+  | None ->
+     let typ = match opt_typ with
+       | None -> Typeops.type_of_constant_type env cb.const_type
+       | Some typ -> typ
+     in
+     let mlt = extract_type env [] 1 typ [] in
+     let schema = (type_maxvar mlt, mlt) in
+     let () = add_cst_type kn cb schema in
+     schema
 
 (*S Extraction of a term. *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 00259750d..da7a4265e 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -143,7 +143,11 @@ let rec pp_expr par env args =
   and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
-	let id = get_db_name n env in apply (pr_id id)
+	let id = get_db_name n env in
+        (* Try to survive to the occurrence of a Dummy rel.
+           TODO: we should get rid of this hack (cf. #592) *)
+        let id = if Id.equal id dummy_name then Id.of_string "__" else id in
+        apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index bfd0794de..62724f211 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -511,6 +511,70 @@ let nb_occur_match =
     | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0
   in nb 1
 
+(* Replace unused variables by _ *)
+
+let dump_unused_vars a =
+  let rec ren env a = match a with
+    | MLrel i ->
+       let () = (List.nth env (i-1)) := true in a
+
+    | MLlam (id,b) ->
+       let occ_id = ref false in
+       let b' = ren (occ_id::env) b in
+       if !occ_id then if b' == b then a else MLlam(id,b')
+       else MLlam(Dummy,b')
+
+    | MLletin (id,b,c) ->
+       let occ_id = ref false in
+       let b' = ren env b in
+       let c' = ren (occ_id::env) c in
+       if !occ_id then
+         if b' == b && c' == c then a else MLletin(id,b',c')
+       else
+         (* 'let' without occurrence: shouldn't happen after simpl *)
+         MLletin(Dummy,b',c')
+
+    | MLcase (t,e,br) ->
+       let e' = ren env e in
+       let br' = Array.smartmap (ren_branch env) br in
+       if e' == e && br' == br then a else MLcase (t,e',br')
+
+    | MLfix (i,ids,v) ->
+       let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in
+       let v' = Array.smartmap (ren env') v in
+       if v' == v then a else MLfix (i,ids,v')
+
+    | MLapp (b,l) ->
+       let b' = ren env b and l' = List.smartmap (ren env) l in
+       if b' == b && l' == l then a else MLapp (b',l')
+
+    | MLcons(t,r,l) ->
+       let l' = List.smartmap (ren env) l in
+       if l' == l then a else MLcons (t,r,l')
+
+    | MLtuple l ->
+       let l' = List.smartmap (ren env) l in
+       if l' == l then a else MLtuple l'
+
+    | MLmagic b ->
+       let b' = ren env b in
+       if b' == b then a else MLmagic b'
+
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> a
+
+    and ren_branch env ((ids,p,b) as tr) =
+      let occs = List.map (fun _ -> ref false) ids in
+      let b' = ren (List.rev_append occs env) b in
+      let ids' =
+        List.map2
+          (fun id occ -> if !occ then id else Dummy)
+          ids occs
+      in
+      if b' == b && List.equal eq_ml_ident ids ids' then tr
+      else (ids',p,b')
+  in
+  ren [] a
+
 (*s Lifting on terms.
     [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *)
 
@@ -949,9 +1013,20 @@ let expand_linear_let o id e =
 
 (* Some beta-iota reductions + simplifications. *)
 
+let rec unmagic = function MLmagic e -> unmagic e | e -> e
+let is_magic = function MLmagic _ -> true | _ -> false
+let magic_hd a = match a with
+  | MLmagic _ :: _ -> a
+  | e :: a -> MLmagic e :: a
+  | [] -> assert false
+
 let rec simpl o = function
   | MLapp (f, []) -> simpl o f
-  | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f)
+  | MLapp (MLapp(f,a),a') -> simpl o (MLapp(f,a@a'))
+  | MLapp (f, a) ->
+     (* When the head of the application is magic, no need for magic on args *)
+     let a = if is_magic f then List.map unmagic a else a in
+     simpl_app o (List.map (simpl o) a) (simpl o f)
   | MLcase (typ,e,br) ->
       let br = Array.map (fun (l,p,t) -> (l,p,simpl o t)) br in
       simpl_case o typ br (simpl o e)
@@ -971,12 +1046,18 @@ let rec simpl o = function
       if ast_occurs_itvl 1 n c.(i) then
 	MLfix (i, ids, Array.map (simpl o) c)
       else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
+  | MLmagic(MLmagic _ as e) -> simpl o e
+  | MLmagic(MLapp (f,l)) -> simpl o (MLapp (MLmagic f, l))
+  | MLmagic(MLletin(id,c,e)) -> simpl o (MLletin(id,c,MLmagic e))
+  | MLmagic(MLcase(typ,e,br)) ->
+     let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in
+     simpl o (MLcase(typ,e,br'))
+  | MLmagic(MLexn _ as e) -> e
   | a -> ast_map (simpl o) a
 
 (* invariant : list [a] of arguments is non-empty *)
 
 and simpl_app o a = function
-  | MLapp (f',a') -> simpl_app o (a'@a) f'
   | MLlam (Dummy,t) ->
       simpl o (MLapp (ast_pop t, List.tl a))
   | MLlam (id,t) -> (* Beta redex *)
@@ -989,8 +1070,9 @@ and simpl_app o a = function
 	     simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
   | MLmagic (MLlam (id,t)) ->
       (* When we've at least one argument, we permute the magic
-         and the lambda, to simplify things a bit (see #2795) *)
-      simpl_app o a (MLlam (id,MLmagic t))
+         and the lambda, to simplify things a bit (see #2795).
+         Alas, the 1st argument must also be magic then. *)
+      simpl_app o (magic_hd a) (MLlam (id,MLmagic t))
   | MLletin (id,e1,e2) when o.opt_let_app ->
       (* Application of a letin: we push arguments inside *)
       MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index c380dfb3e..c07cee713 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -111,6 +111,8 @@ val ast_subst : ml_ast -> ml_ast -> ml_ast
 
 val ast_glob_subst : ml_ast Refmap'.t -> ml_ast -> ml_ast
 
+val dump_unused_vars : ml_ast -> ml_ast
+
 val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
 val inline : global_reference -> ml_ast -> bool
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index e8383bda5..c3dc286cd 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -269,7 +269,7 @@ let rec optim_se top to_appear s = function
       let a = normalize (ast_glob_subst !s a) in
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
-      let d = match optimize_fix a with
+      let d = match dump_unused_vars (optimize_fix a) with
 	| MLfix (0, _, [|c|]) ->
 	  Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
 	| a -> Dterm (r, a, t)
@@ -283,7 +283,8 @@ let rec optim_se top to_appear s = function
 	if inline rv.(i) fake_body
 	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
       done;
-      (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
+      let av' = Array.map dump_unused_vars av in
+      (l,SEdecl (Dfix (rv, av', tv))) :: (optim_se top to_appear s lse)
   | (l,SEmodule m) :: lse ->
       let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
       in (l,SEmodule m) :: (optim_se top to_appear s lse)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 6ff4c25ec..8c86c7711 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -178,7 +178,11 @@ let rec pp_expr par env args =
   and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
-	let id = get_db_name n env in apply (pr_id id)
+	let id = get_db_name n env in
+        (* Try to survive to the occurrence of a Dummy rel.
+           TODO: we should get rid of this hack (cf. #592) *)
+        let id = if Id.equal id dummy_name then Id.of_string "__" else id in
+        apply (pr_id id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 63d792e36..9feaea8cd 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -72,8 +72,6 @@ let mp_length mp =
     | _ -> 1
   in len mp
 
-let visible_con kn = at_toplevel (base_mp (con_modpath kn))
-
 let rec prefixes_mp mp = match mp with
   | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
   | _ -> MPset.singleton mp
@@ -105,17 +103,30 @@ let labels_of_ref r =
 (* Theses tables are not registered within coq save/undo mechanism
    since we reset their contents at each run of Extraction *)
 
-(*s Constants tables. *)
+(* We use [constant_body] (resp. [mutual_inductive_body]) as checksum
+   to ensure that the table contents aren't outdated. *)
 
-let terms = ref (Cmap_env.empty : ml_decl Cmap_env.t)
-let init_terms () = terms := Cmap_env.empty
-let add_term kn d = terms := Cmap_env.add kn d !terms
-let lookup_term kn = Cmap_env.find kn !terms
+(*s Constants tables. *)
 
-let types = ref (Cmap_env.empty : ml_schema Cmap_env.t)
-let init_types () = types := Cmap_env.empty
-let add_type kn s = types := Cmap_env.add kn s !types
-let lookup_type kn = Cmap_env.find kn !types
+let typedefs = ref (Cmap_env.empty : (constant_body * ml_type) Cmap_env.t)
+let init_typedefs () = typedefs := Cmap_env.empty
+let add_typedef kn cb t =
+  typedefs := Cmap_env.add kn (cb,t) !typedefs
+let lookup_typedef kn cb =
+  try
+    let (cb0,t) = Cmap_env.find kn !typedefs in
+    if cb0 == cb then Some t else None
+  with Not_found -> None
+
+let cst_types =
+  ref (Cmap_env.empty : (constant_body * ml_schema) Cmap_env.t)
+let init_cst_types () = cst_types := Cmap_env.empty
+let add_cst_type kn cb s = cst_types := Cmap_env.add kn (cb,s) !cst_types
+let lookup_cst_type kn cb =
+  try
+    let (cb0,s) = Cmap_env.find kn !cst_types in
+    if cb0 == cb then Some s else None
+  with Not_found -> None
 
 (*s Inductives table. *)
 
@@ -124,7 +135,14 @@ let inductives =
 let init_inductives () = inductives := Mindmap_env.empty
 let add_ind kn mib ml_ind =
   inductives := Mindmap_env.add kn (mib,ml_ind) !inductives
-let lookup_ind kn = Mindmap_env.find kn !inductives
+let lookup_ind kn mib =
+  try
+    let (mib0,ml_ind) = Mindmap_env.find kn !inductives in
+    if mib == mib0 then Some ml_ind
+    else None
+  with Not_found -> None
+
+let unsafe_lookup_ind kn = snd (Mindmap_env.find kn !inductives)
 
 let inductive_kinds =
   ref (Mindmap_env.empty : inductive_kind Mindmap_env.t)
@@ -244,10 +262,10 @@ let safe_basename_of_global r =
     | ConstRef kn -> Label.to_id (con_label kn)
     | IndRef (kn,0) -> Label.to_id (mind_label kn)
     | IndRef (kn,i) ->
-      (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename
+      (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename
        with Not_found -> last_chance r)
     | ConstructRef ((kn,i),j) ->
-      (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
+      (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
        with Not_found -> last_chance r)
     | VarRef _ -> assert false
 
@@ -876,6 +894,6 @@ let extract_inductive r s l optstr =
 (*s Tables synchronization. *)
 
 let reset_tables () =
-  init_terms (); init_types (); init_inductives ();
+  init_typedefs (); init_cst_types (); init_inductives ();
   init_inductive_kinds (); init_recursors ();
   init_projs (); init_axioms (); init_opaques (); reset_modfile ()
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index a6734dae8..916cf3ad6 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -55,7 +55,6 @@ val string_of_modfile : module_path -> string
 val file_of_modfile : module_path -> string
 val is_toplevel : module_path -> bool
 val at_toplevel : module_path -> bool
-val visible_con : constant -> bool
 val mp_length : module_path -> int
 val prefixes_mp : module_path -> MPset.t
 val common_prefix_from_list :
@@ -65,14 +64,22 @@ val labels_of_ref : global_reference -> module_path * Label.t list
 
 (*s Some table-related operations *)
 
-val add_term : constant -> ml_decl -> unit
-val lookup_term : constant -> ml_decl
+(* For avoiding repeated extraction of the same constant or inductive,
+   we use cache functions below. Indexing by constant name isn't enough,
+   due to modules we could have a same constant name but different
+   content. So we check that the [constant_body] hasn't changed from
+   recording time to retrieving time. Same for inductive : we store
+   [mutual_inductive_body] as checksum. In both case, we should ideally
+   also check the env *)
 
-val add_type : constant -> ml_schema -> unit
-val lookup_type : constant -> ml_schema
+val add_typedef : constant -> constant_body -> ml_type -> unit
+val lookup_typedef : constant -> constant_body -> ml_type option
+
+val add_cst_type : constant -> constant_body -> ml_schema -> unit
+val lookup_cst_type : constant -> constant_body -> ml_schema option
 
 val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit
-val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind
+val lookup_ind : mutual_inductive -> mutual_inductive_body -> ml_ind option
 
 val add_inductive_kind : mutual_inductive -> inductive_kind -> unit
 val is_coinductive : global_reference -> bool
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 24c0c4749..5cfec1b0d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -257,7 +257,7 @@ let start_dependent_proof id ?pl str goals terminator =
 let get_used_variables () = (cur_pstate ()).section_vars
 let get_universe_binders () = (cur_pstate ()).universe_binders
 
-let proof_using_auto_clear = ref true
+let proof_using_auto_clear = ref false
 let _ = Goptions.declare_bool_option
     { Goptions.optsync  = true;
       Goptions.optdepr  = false;
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 547c9c510..92682fc7a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -347,7 +347,7 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
-let refine_tac {Glob_term.closure=closure;term=term} =
+let refine_tac simple {Glob_term.closure=closure;term=term} =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -363,11 +363,19 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       let (sigma, c) = Pretyping.understand_ltac flags env sigma lvar tycon term in
       Sigma.Unsafe.of_pair (c, sigma)
     end } in
-    Tactics.New.refine ~unsafe:false update
+    let refine = Proofview.Refine.refine ~unsafe:false update in
+    if simple then refine
+    else refine <*>
+           Tactics.New.reduce_after_refine <*>
+           Proofview.shelve_unifiable
   end }
 
 TACTIC EXTEND refine
-  [ "refine" uconstr(c) ] -> [  refine_tac c ]
+| [ "refine" uconstr(c) ] -> [ refine_tac false c ]
+END
+
+TACTIC EXTEND simple_refine
+| [ "simple" "refine" uconstr(c) ] -> [ refine_tac true c ]
 END
 
 (**********************************************************************)
@@ -876,10 +884,11 @@ END
 
 (* Unshelves the goal shelved by the tactic. *)
 TACTIC EXTEND unshelve
-| [ "unshelve" tactic0(t) ] ->
+| [ "unshelve" tactic1(t) ] ->
     [
       Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) ->
-      Proofview.Unsafe.tclNEWGOALS gls
+      Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
+      Proofview.Unsafe.tclSETGOALS (gls @ ogls)
     ]
 END
 
diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v
index a5bea34a9..7a0c3e6f1 100644
--- a/test-suite/bugs/closed/3685.v
+++ b/test-suite/bugs/closed/3685.v
@@ -39,11 +39,11 @@ Module Export PointwiseCore.
              (G : Functor D D')
   : Functor (C -> D) (C' -> D').
   Proof.
-    refine (Build_Functor
+    unshelve (refine (Build_Functor
               (C -> D) (C' -> D')
               _
               _
-              _);
+              _));
     abstract admit.
   Defined.
 End PointwiseCore.
diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v
index b650920b2..df5f66748 100644
--- a/test-suite/bugs/closed/3686.v
+++ b/test-suite/bugs/closed/3686.v
@@ -33,11 +33,11 @@ Module Export PointwiseCore.
              (G : Functor D D')
   : Functor (C -> D) (C' -> D').
   Proof.
-    refine (Build_Functor
+    unshelve (refine (Build_Functor
               (C -> D) (C' -> D')
               _
               _
-              _);
+              _));
     abstract admit.
   Defined.
 End PointwiseCore.
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v
index 62137f0c0..aad0bb44d 100644
--- a/test-suite/bugs/closed/3699.v
+++ b/test-suite/bugs/closed/3699.v
@@ -34,8 +34,8 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -47,8 +47,8 @@ Module NonPrim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intros [a p].
     exact (transport P p (d a)).
   Defined.
@@ -111,8 +111,8 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intro x.
     exact (transport P x.2 (d x.1)).
   Defined.
@@ -124,8 +124,8 @@ Module Prim.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim _ _)).
-    2:exact b.
+    unshelve (refine (pr1 (isconnected_elim _ _))).
+    exact b.
     intros [a p].
     exact (transport P p (d a)).
   Defined.
diff --git a/test-suite/bugs/opened/3923.v b/test-suite/bugs/closed/3923.v
index 6aa6b4932..0aa029e73 100644
--- a/test-suite/bugs/opened/3923.v
+++ b/test-suite/bugs/closed/3923.v
@@ -30,4 +30,4 @@ Axiom empty_fieldstore : cert_fieldstore.
 
 End MkCertRuntimeTypes.
 
-Fail Extraction MkCertRuntimeTypes.
+Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *)
diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v
index f808cb45e..5932c9c56 100644
--- a/test-suite/bugs/closed/4116.v
+++ b/test-suite/bugs/closed/4116.v
@@ -110,7 +110,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type :=
   Trunc_is_trunc : IsTrunc_internal n A.
 
 Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" :=
-  refine (let __transparent_assert_hypothesis := (_ : type) in _);
+  unshelve refine (let __transparent_assert_hypothesis := (_ : type) in _);
   [
       | (
         let H := match goal with H := _ |- _ => constr:(H) end in
@@ -321,7 +321,7 @@ Section Grothendieck.
 
   Definition Gcategory : PreCategory.
   Proof.
-    refine (@Build_PreCategory
+    unshelve refine (@Build_PreCategory
               Pair
               (fun s d => Gmorphism s d)
               Gidentity
@@ -346,7 +346,7 @@ Section Grothendieck2.
   Instance iscategory_grothendieck_toset : IsCategory (Gcategory F).
   Proof.
     intros s d.
-    refine (isequiv_adjointify _ _ _ _).
+    unshelve refine (isequiv_adjointify _ _ _ _).
     {
       intro m.
       transparent assert (H' : (s.(c) = d.(c))).
diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v
index e86b3be64..ea3347a85 100644
--- a/test-suite/bugs/closed/931.v
+++ b/test-suite/bugs/closed/931.v
@@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop.
 
 Goal Prop.
   refine (P _ _).
-  2:instantiate (1:=0).
+    instantiate (1:=0).
   trivial.
 Qed.
diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v
index 5fa167038..d77b9b63a 100644
--- a/test-suite/bugs/closed/HoTT_coq_090.v
+++ b/test-suite/bugs/closed/HoTT_coq_090.v
@@ -84,7 +84,7 @@ Arguments transport {A} P {x y} p%path_scope u : simpl nomatch.
 Instance isequiv_path {A B : Type} (p : A = B)
   : IsEquiv (transport (fun X:Type => X) p) | 0.
 Proof.
-  refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
+  unshelve refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _);
   admit.
 Defined.
 
diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out
index 848abd009..f738b0d09 100644
--- a/test-suite/output/Extraction_matchs_2413.out
+++ b/test-suite/output/Extraction_matchs_2413.out
@@ -4,7 +4,7 @@ let test1 b =
   b
 (** val test2 : bool -> bool **)
 
-let test2 b =
+let test2 _ =
   False
 (** val wrong_id : 'a1 hole -> 'a2 hole **)
 
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index c83f45e2a..adaa05ad0 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -178,6 +178,7 @@ End Let.
 
 Check (test_let 3).
 
+(* Disabled
 Section Clear.
 
 Variable a: nat.
@@ -192,6 +193,6 @@ trivial.
 Qed.
 
 End Clear.
-
+*)
 
 
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 1e667884b..352abb2af 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -62,7 +62,7 @@ Abort.
 Goal (forall n : nat, n = 0 -> Prop) -> Prop.
 intro P.
  refine (P _ _).
-2:reflexivity.
+reflexivity.
 Abort.
 
 (* Submitted by Jacek Chrzaszcz (bug #1102) *)
diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v
new file mode 100644
index 000000000..672222bdd
--- /dev/null
+++ b/test-suite/success/unshelve.v
@@ -0,0 +1,11 @@
+Axiom F : forall (b : bool), b = true ->
+  forall (i : unit), i = i -> True.
+
+Goal True.
+Proof.
+unshelve (refine (F _ _ _ _)).
++ exact true.
++ exact tt.
++ exact (@eq_refl bool true).
++ exact (@eq_refl unit tt).
+Qed.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 45306caf0..aa9df50a7 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -970,6 +970,7 @@ Section Map.
   Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
     In y (flat_map f l) <-> exists x, In x l /\ In y (f x).
   Proof using A B.
+    clear Hfinjective.
     induction l; simpl; split; intros.
     contradiction.
     destruct H as (x,(H,_)); contradiction.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index d4ebfb42f..2ae0ade80 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -444,10 +444,10 @@ Section Proof_irrelevance_WEM_CC.
   Theorem wproof_irrelevance_cc : ~~(b1 = b2).
   Proof.
     intros h.
-    refine (let NB := exist (fun P=>~~P -> P) B _ in _).
+    unshelve (refine (let NB := exist (fun P=>~~P -> P) B _ in _)).
     { exact (fun _ => b1). }
     pose proof (NoRetractToNegativeProp.paradox NB p2b b2p (wp2p2 h) wp2p1) as paradox.
-    refine (let F := exist (fun P=>~~P->P) False _ in _).
+    unshelve (refine (let F := exist (fun P=>~~P->P) False _ in _)).
     { auto. }
     exact (paradox F).
   Qed.
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 4e582934a..5c87011e5 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -266,7 +266,7 @@ End Paradox.
 
 (** The [paradox] tactic can be called as a shortcut to use the paradox. *)
 Ltac paradox h :=
-  refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ));cycle 1.
+  unshelve (refine ((fun h => _) (paradox _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ))).
 
 End Generic.
 
@@ -319,25 +319,26 @@ Proof.
   + cbn. exact (fun u F => forall x:u, F x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. easy.
+
   + cbn. exact (fun F => u22u1 (forall x, F x)).
   + cbn. exact (fun _ x => u22u1_unit _ x).
   + cbn. exact (fun _ x => u22u1_counit _ x).
-  + cbn. intros **. now rewrite u22u1_coherent.
   (** Small universe *)
   + exact U0.
   (** The interpretation of the small universe is the image of
       [U0] in [U1]. *)
   + cbn. exact (fun X => u02u1 X).
   + cbn. exact (fun u F => u12u0 (forall x:(u02u1 u), u02u1 (F x))).
-  + cbn. intros * x. exact (u12u0_unit _ x).
-  + cbn. intros * x. exact (u12u0_counit _ x).
   + cbn. exact (fun u F => u12u0 (forall x:u, u02u1 (F x))).
-  + cbn. intros * x. exact (u12u0_unit _ x).
-  + cbn. intros * x. exact (u12u0_counit _ x).
   + cbn. exact (u12u0 F).
   + cbn in h.
     exact (u12u0_counit _ h).
+  + cbn. easy.
+  + cbn. intros **. now rewrite u22u1_coherent.
+  + cbn. intros * x. exact (u12u0_unit _ x).
+  + cbn. intros * x. exact (u12u0_counit _ x).
+  + cbn. intros * x. exact (u12u0_unit _ x).
+  + cbn. intros * x. exact (u12u0_counit _ x).
 Qed.
 
 End Paradox.
@@ -381,7 +382,7 @@ Qed.
 
 Definition Forall {A:Type} (P:A->MProp) : MProp.
 Proof.
-  refine (exist _ _ _).
+  unshelve (refine (exist _ _ _)).
   + exact (forall x:A, El (P x)).
   + intros h x.
     eapply strength in h.
@@ -411,27 +412,27 @@ Proof.
   + exact (fun _ => Forall).
   + cbn. exact (fun _ _ f => f).
   + cbn. exact (fun _ _ f => f).
-  + cbn. easy.
   + exact Forall.
   + cbn. exact (fun _ f => f).
   + cbn. exact (fun _ f => f).
-  + cbn. easy.
   (** Small universe *)
   + exact bool.
   + exact (fun b => El (b2p b)).
   + cbn. exact (fun _ F => p2b (Forall (fun x => b2p (F x)))).
+  + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))).
+  + apply p2b.
+    exact B.
+  + cbn in h. auto.
+  + cbn. easy.
+  + cbn. easy.
   + cbn. auto.
   + cbn. intros * f.
     apply p2p1 in f. cbn in f.
     exact f.
-  + exact (fun _ F => p2b (Forall (fun x => b2p (F x)))).
   + cbn. auto.
   + cbn. intros * f.
     apply p2p1 in f. cbn in f.
     exact f.
-  + apply p2b.
-    exact B.
-  + cbn in h. auto.
 Qed.
 
 End Paradox.
@@ -469,18 +470,18 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
 Theorem paradox : forall B:NProp, El B.
 Proof.
   intros B.
-  refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))).
   + exact (fun P => ~~P).
-  + cbn. auto.
-  + cbn. auto.
-  + cbn. auto.
   + exact bool.
   + exact p2b.
   + exact b2p.
-  + auto.
-  + auto.
   + exact B.
   + exact h.
+  + cbn. auto.
+  + cbn. auto.
+  + cbn. auto.
+  + auto.
+  + auto.
 Qed.
 
 End Paradox.
@@ -515,18 +516,18 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
 Theorem mparadox : forall B:NProp, El B.
 Proof.
   intros B.
-  refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _));cycle 1.
+  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))).
   + exact (fun P => P).
-  + cbn. auto.
-  + cbn. auto.
-  + cbn. auto.
   + exact bool.
   + exact p2b.
   + exact b2p.
-  + auto.
-  + auto.
   + exact B.
   + exact h.
+  + cbn. auto.
+  + cbn. auto.
+  + cbn. auto.
+  + auto.
+  + auto.
 Qed.
 
 End MParadox.
@@ -548,8 +549,8 @@ Hypothesis p2p2 : forall A:Prop, A -> b2p (p2b A).
 Theorem paradox : forall B:Prop, B.
 Proof.
   intros B.
-  refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
-                   (exist _ B (fun x => x))).
+  unshelve (refine (mparadox (exist _ bool (fun x => x)) _ _ _ _
+                   (exist _ B (fun x => x)))).
   + intros p. red. red. exact (p2b (El p)).
   + cbn. intros b. red. exists (b2p b). exact (fun x => x).
   + cbn. intros [A H]. cbn. apply p2p1.
@@ -596,7 +597,6 @@ Proof.
   + cbn. exact (fun u F => forall x, F x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. easy.
   + exact (fun F => forall A:Prop, F(up A)).
   + cbn. exact (fun F f A => f (up A)).
   + cbn.
@@ -604,20 +604,21 @@ Proof.
     specialize (f (down A)).
     rewrite up_down in f.
     exact f.
+  + exact Prop.
+  + cbn. exact (fun X => X).
+  + cbn. exact (fun A P => forall x:A, P x).
+  + cbn. exact (fun A P => forall x:A, P x).
+  + cbn. exact P.
+  + exact h.
+  + cbn. easy.
   + cbn.
     intros F f A.
     destruct (up_down A). cbn.
     reflexivity.
-  + exact Prop.
-  + cbn. exact (fun X => X).
-  + cbn. exact (fun A P => forall x:A, P x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. exact (fun A P => forall x:A, P x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. exact P.
-  + exact h.
 Qed.
 
 End Paradox.
@@ -664,37 +665,37 @@ Proof.
   + cbn. exact (fun X F => forall x:X, F x).
   + cbn. exact (fun _ _ x => x).
   + cbn. exact (fun _ _ x => x).
-  + cbn. easy.
   + exact (fun F => forall x:A, F (up x)).
   + cbn. exact (fun _ f => fun x:A => f (up x)).
   + cbn. intros * f X.
     specialize (f (down X)).
     rewrite up_down in f.
     exact f.
-  + cbn. intros ? f X.
-    destruct (up_down X). cbn.
-    reflexivity.
   (** Small universe *)
   + exact A.
   (** The interpretation of [A] as a universe is [U]. *)
   + cbn. exact up.
   + cbn. exact (fun _ F => down (forall x, up (F x))).
+  + cbn. exact (fun _ F => down (forall x, up (F x))).
+  + cbn. exact (down False).
+  + rewrite up_down in p.
+    exact p.
+  + cbn. easy.
+  + cbn. intros ? f X.
+    destruct (up_down X). cbn.
+    reflexivity.
   + cbn. intros ? ? f.
     rewrite up_down.
     exact f.
   + cbn. intros ? ? f.
     rewrite up_down in f.
     exact f.
-  + cbn. exact (fun _ F => down (forall x, up (F x))).
   + cbn. intros ? ? f.
     rewrite up_down.
     exact f.
   + cbn. intros ? ? f.
     rewrite up_down in f.
     exact f.
-  + cbn. exact (down False).
-  + rewrite up_down in p.
-    exact p.
 Qed.
 
 End Paradox.
@@ -710,7 +711,7 @@ Module PropNeqType.
 Theorem paradox : Prop <> Type.
 Proof.
   intros h.
-  refine (TypeNeqSmallType.paradox _ _).
+  unshelve (refine (TypeNeqSmallType.paradox _ _)).
   + exact Prop.
   + easy.
 Qed.