27 files changed, 349 insertions, 237 deletions

diff --git a/.gitattributes b/.gitattributes
index e087e1737..a5edcdb5b 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -5,48 +5,51 @@
 # Because our commit hook automatically does [apply whitespace=fix] we
 # disable whitespace checking for all files except those where we want
 # it. Otherwise rogue global configuration and forgotten local
-# configuration can break commits.
+# configuration can break commits. Note that git cannot fix but can
+# detect a blank-at-eof when it comes from removing a chunk of text at
+# the end of the file, leaving an extra newline from before that
+# chunk, so we disable blank-at-eof.
 * -whitespace
 
 # tabs are allowed in Makefiles.
-Makefile* whitespace=trailing-space
-tools/CoqMakefile.in whitespace=trailing-space
+Makefile* whitespace=blank-at-eol
+tools/CoqMakefile.in whitespace=blank-at-eol
 
 # in general we don't want tabs.
-*.asciidoc whitespace=trailing-space,tab-in-indent
-*.bib whitespace=trailing-space,tab-in-indent
-*.c whitespace=trailing-space,tab-in-indent
-*.css whitespace=trailing-space,tab-in-indent
-*.dtd whitespace=trailing-space,tab-in-indent
-*.el whitespace=trailing-space,tab-in-indent
-*.g whitespace=trailing-space,tab-in-indent
-*.h whitespace=trailing-space,tab-in-indent
-*.html whitespace=trailing-space,tab-in-indent
-*.hva whitespace=trailing-space,tab-in-indent
-*.js whitespace=trailing-space,tab-in-indent
-*.json whitespace=trailing-space,tab-in-indent
-*.lang whitespace=trailing-space,tab-in-indent
-*.md whitespace=trailing-space,tab-in-indent
-*.merlin whitespace=trailing-space,tab-in-indent
-*.ml whitespace=trailing-space,tab-in-indent
-*.ml4 whitespace=trailing-space,tab-in-indent
-*.mli whitespace=trailing-space,tab-in-indent
-*.mll whitespace=trailing-space,tab-in-indent
-*.mllib whitespace=trailing-space,tab-in-indent
-*.mlp whitespace=trailing-space,tab-in-indent
-*.mlpack whitespace=trailing-space,tab-in-indent
-*.nsh whitespace=trailing-space,tab-in-indent
-*.nsi whitespace=trailing-space,tab-in-indent
-*.py whitespace=trailing-space,tab-in-indent
-*.rst whitespace=trailing-space,tab-in-indent
-*.sh whitespace=trailing-space,tab-in-indent
-*.sty whitespace=trailing-space,tab-in-indent
-*.tex whitespace=trailing-space,tab-in-indent
-*.tokens whitespace=trailing-space,tab-in-indent
-*.txt whitespace=trailing-space,tab-in-indent
-*.v whitespace=trailing-space,tab-in-indent
-*.xml whitespace=trailing-space,tab-in-indent
-*.yml whitespace=trailing-space,tab-in-indent
+*.asciidoc whitespace=blank-at-eol,tab-in-indent
+*.bib whitespace=blank-at-eol,tab-in-indent
+*.c whitespace=blank-at-eol,tab-in-indent
+*.css whitespace=blank-at-eol,tab-in-indent
+*.dtd whitespace=blank-at-eol,tab-in-indent
+*.el whitespace=blank-at-eol,tab-in-indent
+*.g whitespace=blank-at-eol,tab-in-indent
+*.h whitespace=blank-at-eol,tab-in-indent
+*.html whitespace=blank-at-eol,tab-in-indent
+*.hva whitespace=blank-at-eol,tab-in-indent
+*.js whitespace=blank-at-eol,tab-in-indent
+*.json whitespace=blank-at-eol,tab-in-indent
+*.lang whitespace=blank-at-eol,tab-in-indent
+*.md whitespace=blank-at-eol,tab-in-indent
+*.merlin whitespace=blank-at-eol,tab-in-indent
+*.ml whitespace=blank-at-eol,tab-in-indent
+*.ml4 whitespace=blank-at-eol,tab-in-indent
+*.mli whitespace=blank-at-eol,tab-in-indent
+*.mll whitespace=blank-at-eol,tab-in-indent
+*.mllib whitespace=blank-at-eol,tab-in-indent
+*.mlp whitespace=blank-at-eol,tab-in-indent
+*.mlpack whitespace=blank-at-eol,tab-in-indent
+*.nsh whitespace=blank-at-eol,tab-in-indent
+*.nsi whitespace=blank-at-eol,tab-in-indent
+*.py whitespace=blank-at-eol,tab-in-indent
+*.rst whitespace=blank-at-eol,tab-in-indent
+*.sh whitespace=blank-at-eol,tab-in-indent
+*.sty whitespace=blank-at-eol,tab-in-indent
+*.tex whitespace=blank-at-eol,tab-in-indent
+*.tokens whitespace=blank-at-eol,tab-in-indent
+*.txt whitespace=blank-at-eol,tab-in-indent
+*.v whitespace=blank-at-eol,tab-in-indent
+*.xml whitespace=blank-at-eol,tab-in-indent
+*.yml whitespace=blank-at-eol,tab-in-indent
 
 # CR is desired for these Windows files.
-*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent
+*.bat whitespace=cr-at-eol,blank-at-eol,tab-in-indent
diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh
new file mode 100644
index 000000000..e6c48d10a
--- /dev/null
+++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then
+    Equations_CI_BRANCH=unification-returns-option
+    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh
new file mode 100644
index 000000000..6939ead2b
--- /dev/null
+++ b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then
+
+    # this branch contains a commit not present on coq-master that triggers
+    # the universe restriction bug #7472
+    Elpi_CI_BRANCH=overlay-7495
+    Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 4838dd734..bb8189efc 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -28,6 +28,10 @@ Proof engine
   should indicate what the canonical form is. An important change is
   the move of `Globnames.global_reference` to `Names.GlobRef.t`.
 
+- Unification API returns `evar_map option` instead of `bool * evar_map`
+  with the guarantee that the `evar_map` was unchanged if the boolean
+  was false.
+
 ML Libraries used by Coq
 
 - Introduction of a "Smart" module for collecting "smart*" functions, e.g.
diff --git a/engine/univops.ml b/engine/univops.ml
index 76dbaa250..3fd518490 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -35,79 +35,14 @@ let universes_of_constr env c =
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
 
-type graphnode = {
-  mutable up : constraint_type LMap.t;
-  mutable visited : bool
-}
-
-let merge_types d d0 =
-  match d, d0 with
-  | _, Lt | Lt, _ -> Lt
-  | Le, _ | _, Le -> Le
-  | Eq, Eq -> Eq
-
-let merge_up d b up =
-  let find = try Some (LMap.find b up) with Not_found -> None in
-  match find with
-  | Some d0 ->
-    let d = merge_types d d0 in
-    if d == d0 then up else LMap.add b d up
-  | None -> LMap.add b d up
-
-let add_up a d b graph =
-  let node, graph =
-    try LMap.find a graph, graph
-    with Not_found ->
-      let node = { up = LMap.empty; visited = false } in
-      node, LMap.add a node graph
-  in
-  node.up <- merge_up d b node.up;
-  graph
-
-(* for each node transitive close until you find a non removable, discard the rest *)
-let transitive_close removable graph =
-  let rec do_node a node =
-    if not node.visited
-    then
-      let keepup =
-        LMap.fold (fun b d keepup ->
-            if not (LSet.mem b removable)
-            then merge_up d b keepup
-            else
-              begin
-                match LMap.find b graph with
-                | bnode ->
-                  do_node b bnode;
-                  LMap.fold (fun k d' keepup ->
-                    merge_up (merge_types d d') k keepup)
-                    bnode.up keepup
-                | exception Not_found -> keepup
-              end
-          )
-          node.up LMap.empty
-      in
-      node.up <- keepup;
-      node.visited <- true
-  in
-  LMap.iter do_node graph
-
-let restrict_universe_context (univs,csts) keep =
-  let removable = LSet.diff univs keep in
-  let (csts, rem) =
-    Constraint.fold (fun (a,d,b as cst) (csts, rem) ->
-        if LSet.mem a removable || LSet.mem b removable
-        then (csts, add_up a d b rem)
-        else (Constraint.add cst csts, rem))
-      csts (Constraint.empty, LMap.empty)
-  in
-  transitive_close removable rem;
-  let csts =
-    LMap.fold (fun a node csts ->
-        if LSet.mem a removable
-        then csts
-        else
-          LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts)
-            node.up csts)
-      rem csts
-  in
+let restrict_universe_context (univs, csts) keep =
+  let removed = LSet.diff univs keep in
+  if LSet.is_empty removed then univs, csts
+  else
+  let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in
+  let g = UGraph.empty_universes in
+  let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in
+  let g = UGraph.merge_constraints csts g in
+  let allkept = LSet.diff allunivs removed in
+  let csts = UGraph.constraints_for ~kept:allkept g in
   (LSet.inter univs keep, csts)
diff --git a/engine/univops.mli b/engine/univops.mli
index d1585414c..0b37ab975 100644
--- a/engine/univops.mli
+++ b/engine/univops.mli
@@ -14,5 +14,8 @@ open Univ
 (** The universes of monomorphic constants appear. *)
 val universes_of_constr : Environ.env -> constr -> LSet.t
 
-(** Shrink a universe context to a restricted set of variables *)
+(** [restrict_universe_context (univs,csts) keep] restricts [univs] to
+   the universes in [keep]. The constraints [csts] are adjusted so
+   that transitive constraints between remaining universes (those in
+   [keep] and those not in [univs]) are preserved. *)
 val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8f83d6baa..c11b9ebf4 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -479,6 +479,34 @@ let iter_with_binders g f n c = match kind c with
       Array.Fun1.iter f n tl;
       Array.Fun1.iter f (iterate g (Array.length tl) n) bl
 
+(* [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
+   subterms of [c] starting from [acc] and proceeding from left to
+   right according to the usual representation of the constructions as
+   [fold_constr] but it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive *)
+
+let fold_constr_with_binders g f n acc c =
+  match kind c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> acc
+  | Cast (c,_, t) -> f n (f n acc c) t
+  | Prod (na,t,c) -> f (g  n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g  n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g  n) (f n (f n acc b) t) c
+  | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+  | Proj (p,c) -> f n acc c
+  | Evar (_,l) -> Array.fold_left (f n) acc l
+  | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+  | Fix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+  | CoFix (_,(lna,tl,bl)) ->
+      let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in
+      let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+      Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
 (* [map f c] maps [f] on the immediate subterms of [c]; it is
    not recursive and the order with which subterms are processed is
    not specified *)
diff --git a/kernel/constr.mli b/kernel/constr.mli
index b35ea6653..742a13919 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -402,6 +402,15 @@ val iter : (constr -> unit) -> constr -> unit
 val iter_with_binders :
   ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit
 
+(** [iter_with_binders g f n c] iters [f n] on the immediate
+   subterms of [c]; it carries an extra data [n] (typically a lift
+   index) which is processed by [g] (which typically add 1 to [n]) at
+   each binder traversal; it is not recursive and the order with which
+   subterms are processed is not specified *)
+
+val fold_constr_with_binders :
+  ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
+
 type constr_compare_fn = int -> constr -> constr -> bool
 
 (** [compare_head f c1 c2] compare [c1] and [c2] using [f] to compare
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 036cd4847..5174eeea8 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2017,21 +2017,22 @@ let compile_mind_deps env prefix ~interactive
 
 (* This function compiles all necessary dependencies of t, and generates code in
    reverse order, as well as linking information updates *)
-let rec compile_deps env sigma prefix ~interactive init t =
+let compile_deps env sigma prefix ~interactive init t =
+  let rec aux env lvl init t =
   match kind t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
-      let c,u = get_alias env c in
-      let cb,(nameref,_) = lookup_constant_key c env in
-      let (_, (_, const_updates)) = init in
-      if is_code_loaded ~interactive nameref
-        || (Cmap_env.mem c const_updates)
-      then init
-      else
+    let c,u = get_alias env c in
+    let cb,(nameref,_) = lookup_constant_key c env in
+    let (_, (_, const_updates)) = init in
+    if is_code_loaded ~interactive nameref
+    || (Cmap_env.mem c const_updates)
+    then init
+    else
       let comp_stack, (mind_updates, const_updates) =
 	match cb.const_proj, cb.const_body with
         | false, Def t ->
-	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+           aux env lvl init (Mod_subst.force_constr t)
         | true, _ ->
           let pb = lookup_projection (Projection.make c false) env in
           let mind = pb.proj_ind in
@@ -2047,12 +2048,30 @@ let rec compile_deps env sigma prefix ~interactive init t =
   | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
     let term = mkApp (mkConst (Projection.constant p), [|c|]) in
-      compile_deps env sigma prefix ~interactive init term
+    aux env lvl init term
   | Case (ci, p, c, ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
-      Constr.fold (compile_deps env sigma prefix ~interactive) init t
-  | _ -> Constr.fold (compile_deps env sigma prefix ~interactive) init t
+      fold_constr_with_binders succ (aux env) lvl init t
+  | Var id ->
+    let open Context.Named.Declaration in
+    begin match lookup_named id env with
+      | LocalDef (_,t,_) ->
+        aux env lvl init t
+      | _ -> init
+    end
+  | Rel n when n > lvl ->
+    let open Context.Rel.Declaration in
+    let decl = lookup_rel n env in
+    let env = env_of_rel n env in
+    begin match decl with
+    | LocalDef (_,t,_) ->
+      aux env lvl init t
+    | LocalAssum _ -> init
+    end
+  | _ -> fold_constr_with_binders succ (aux env) lvl init t
+  in
+  aux env 0 init t
 
 let compile_constant_field env prefix con acc cb =
     let (gl, _) =
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 8b61ed0c5..6db75c89a 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -296,15 +296,17 @@ let is_value lc =
   match lc with
   | Lval _ -> true
   | Lmakeblock(_,_,_,args) when Array.is_empty args -> true
+  | Luint (UintVal _) -> true
   | _ -> false
-	
+
 let get_value lc =
   match lc with
   | Lval v -> v
-  | Lmakeblock(_,_,tag,args) when Array.is_empty args -> 
+  | Lmakeblock(_,_,tag,args) when Array.is_empty args ->
       Nativevalues.mk_int tag
+  | Luint (UintVal i) -> Nativevalues.mk_uint i
   | _ -> raise Not_found
-	
+
 let make_args start _end =
   Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
     
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index e6b27077b..4a9467de5 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -503,7 +503,7 @@ let insert_edge strict ucan vcan g =
     let () = cleanup_universes g in
     raise e
 
-let add_universe vlev strict g =
+let add_universe_gen vlev g =
   try
     let _arcv = UMap.find vlev g.entries in
       raise AlreadyDeclared
@@ -520,8 +520,14 @@ let add_universe vlev strict g =
     }
     in
     let entries = UMap.add vlev (Canonical v) g.entries in
-    let g = { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges } in
-    insert_edge strict (get_set_arc g) v g
+    { entries; index = g.index - 1; n_nodes = g.n_nodes + 1; n_edges = g.n_edges }, v
+
+let add_universe vlev strict g =
+  let g, v = add_universe_gen vlev g in
+  insert_edge strict (get_set_arc g) v g
+
+let add_universe_unconstrained vlev g =
+  fst (add_universe_gen vlev g)
 
 exception Found_explanation of explanation
 
@@ -696,6 +702,9 @@ let enforce_univ_lt u v g =
     error_inconsistency Lt u v (get_explanation false v u g)
 
 let empty_universes =
+  { entries = UMap.empty; index = 0; n_nodes = 0; n_edges = 0 }
+
+let initial_universes =
   let set_arc = Canonical {
     univ = Level.set;
     ltle = LMap.empty;
@@ -718,9 +727,6 @@ let empty_universes =
   let empty = { entries; index = (-2); n_nodes = 2; n_edges = 0 } in
   enforce_univ_lt Level.prop Level.set empty
 
-(* Prop = Set is forbidden here. *)
-let initial_universes = empty_universes
-
 let is_initial_universes g = UMap.equal (==) g.entries initial_universes.entries
 
 let enforce_constraint cst g =
@@ -780,6 +786,42 @@ let constraints_of_universes g =
   let csts = UMap.fold constraints_of g.entries Constraint.empty in
   csts, UF.partition uf
 
+(* domain g.entries = kept + removed *)
+let constraints_for ~kept g =
+  (* rmap: partial map from canonical universes to kept universes *)
+  let rmap, csts = LSet.fold (fun u (rmap,csts) ->
+      let arcu = repr g u in
+      if LSet.mem arcu.univ kept then
+        LMap.add arcu.univ arcu.univ rmap, enforce_eq_level u arcu.univ csts
+      else
+        match LMap.find arcu.univ rmap with
+        | v -> rmap, enforce_eq_level u v csts
+        | exception Not_found -> LMap.add arcu.univ u rmap, csts)
+      kept (LMap.empty,Constraint.empty)
+  in
+  let rec add_from u csts todo = match todo with
+    | [] -> csts
+    | (v,strict)::todo ->
+      let v = repr g v in
+      (match LMap.find v.univ rmap with
+       | v ->
+         let d = if strict then Lt else Le in
+         let csts = Constraint.add (u,d,v) csts in
+         add_from u csts todo
+       | exception Not_found ->
+         (* v is not equal to any kept universe *)
+         let todo = LMap.fold (fun v' strict' todo ->
+             (v',strict || strict') :: todo)
+             v.ltle todo
+         in
+         add_from u csts todo)
+  in
+  LSet.fold (fun u csts ->
+      let arc = repr g u in
+      LMap.fold (fun v strict csts -> add_from u csts [v,strict])
+        arc.ltle csts)
+    kept csts
+
 (** [sort_universes g] builds a totally ordered universe graph.  The
     output graph should imply the input graph (and the implication
     will be strict most of the time), but is not necessarily minimal.
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index cca2eb472..e6dd629e4 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -49,13 +49,15 @@ exception AlreadyDeclared
 
 val add_universe : Level.t -> bool -> t -> t
 
+(** Add a universe without (Prop,Set) <= u *)
+val add_universe_unconstrained : Level.t -> t -> t
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t
 
 (** The empty graph of universes *)
 val empty_universes : t
-[@@ocaml.deprecated "Use UGraph.initial_universes"]
 
 val sort_universes : t -> t
 
@@ -64,6 +66,12 @@ val sort_universes : t -> t
    of the universes into equivalence classes. *)
 val constraints_of_universes : t -> Constraint.t * LSet.t list
 
+(** [constraints_for ~kept g] returns the constraints about the
+   universes [kept] in [g] up to transitivity.
+
+    eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *)
+val constraints_for : kept:LSet.t -> t -> Constraint.t
+
 val check_subtype : AUContext.t check_function
 (** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
     [ctx1]. *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 062136ff5..6d08f66c1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -366,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
   let ground_test =
     if is_ground_term evd term1 && is_ground_term evd term2 then (
       let e =
-	try
-	  let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
-	    env evd term1 term2
-	  in
-	    if b then Success evd
-	    else UnifFailure (evd, ConversionFailed (env,term1,term2))
-	with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
+          match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with
+          | Some evd -> Success evd
+          | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))
+          | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
       in
 	match e with
 	| UnifFailure (evd, e) when not (is_ground_env evd env) -> None
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 67b7a2a40..4997d0bf0 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -25,4 +25,4 @@ val native_norm : env -> evar_map -> constr -> types -> constr
 
 (** Conversion with inference of universe constraints *)
 val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool
+  evar_map option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 92f87ab95..b2507b5f2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1082,9 +1082,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
 	      if not (occur_existential !evdref cty || occur_existential !evdref tval) then
-		let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
-		if b then (evdref := evd; cj, tval)
-		else
+                match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with
+                | Some evd -> (evdref := evd; cj, tval)
+                | None ->
 		  error_actual_type ?loc env.ExtraEnv.env !evdref cj tval 
                       (ConversionFailed (env.ExtraEnv.env,cty,tval))
 	      else user_err ?loc  (str "Cannot check cast with vm: " ++
@@ -1093,9 +1093,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
             begin
-	      let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
-	      if b then (evdref := evd; cj, tval)
-	      else
+              match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with
+              | Some evd -> (evdref := evd; cj, tval)
+              | None ->
                 error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
                   (ConversionFailed (env.ExtraEnv.env,cty,tval))
             end
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6fde86837..7fb1a0a57 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
     ?(ts=full_transparent_state) env sigma x y =
   (** FIXME *)
   try
-    let b, sigma = 
-      let ans =
-	if pb == Reduction.CUMUL then 
+      let ans = match pb with
+      | Reduction.CUMUL ->
           EConstr.leq_constr_universes env sigma x y
-	else
+      | Reduction.CONV ->
           EConstr.eq_constr_universes env sigma x y
       in
       let ans = match ans with
@@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
         with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None
       in
       match ans with
-      | None -> false, sigma
-      | Some sigma -> true, sigma
-    in
-      if b then sigma, true
-      else
+      | Some sigma -> ans
+      | None ->
         let x = EConstr.Unsafe.to_constr x in
         let y = EConstr.Unsafe.to_constr y in
 	let sigma' = 
 	  conv_fun pb ~l2r:false sigma ts
 	    env (sigma, sigma_univ_state) x y in
-	  sigma', true
+        Some sigma'
   with
-  | Reduction.NotConvertible -> sigma, false
-  | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
+  | Reduction.NotConvertible -> None
+  | Univ.UniverseInconsistency _ when catch_incon -> None
   | e when is_anomaly e -> report_anomaly e
 
 let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ad280d9f3..9256fa7ce 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -277,13 +277,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env ->  evar_map -> con
     otherwise returns false in that case.
  *)
 val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> 
-  env -> evar_map -> constr -> constr -> evar_map * bool
+  env -> evar_map -> constr -> constr -> evar_map option
 
 (** Conversion with inference of universe constraints *)
 val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool) -> unit
+  evar_map option) -> unit
 val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
-  evar_map * bool
+  evar_map option
 
 
 (** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
@@ -291,7 +291,7 @@ conversion function. Used to pretype vm and native casts. *)
 val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
     (Constr.constr, evar_map) Reduction.generic_conversion_function) ->
   ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
-  evar_map -> constr -> constr -> evar_map * bool
+  evar_map -> constr -> constr -> evar_map option
 
 (** {6 Special-Purpose Reduction Functions } *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5f7faa13e..a8a4003dc 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -579,16 +579,16 @@ let constr_cmp pb env sigma flags t u =
   in 
   match cstrs with
   | Some cstrs ->
-      begin try Evd.add_universe_constraints sigma cstrs, true
-      with Univ.UniverseInconsistency _ -> sigma, false
+      begin try Some (Evd.add_universe_constraints sigma cstrs)
+      with Univ.UniverseInconsistency _ -> None
       | Evd.UniversesDiffer -> 
 	if is_rigid_head sigma flags t then 
-          try Evd.add_universe_constraints sigma (force_eqs cstrs), true
-	  with Univ.UniverseInconsistency _ -> sigma, false
-	else sigma, false
+          try Some (Evd.add_universe_constraints sigma (force_eqs cstrs))
+          with Univ.UniverseInconsistency _ -> None
+        else None
       end
   | None ->
-    sigma, false
+    None
     
 let do_reduce ts (env, nb) sigma c =
   Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
@@ -623,9 +623,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM
   | None -> sigma
   | Some n ->
     if is_ground_term sigma m && is_ground_term sigma n then
-      let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in
-	if b then sigma
-	else error_cannot_unify env sigma (m,n)
+      match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with
+      | Some sigma -> sigma
+      | None -> error_cannot_unify env sigma (m,n)
     else sigma
 
 
@@ -740,11 +740,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	| Evar (evk,_ as ev), Evar (evk',_)
             when not (Evar.Set.mem evk flags.frozen_evars)
               && Evar.equal evk evk' ->
-            let sigma',b = constr_cmp cv_pb env sigma flags cM cN in
-            if b then
-	      sigma',metasubst,evarsubst
-            else
+            begin match constr_cmp cv_pb env sigma flags cM cN with
+            | Some sigma ->
+              sigma, metasubst, evarsubst
+            | None ->
 	      sigma,metasubst,((curenv,ev,cN)::evarsubst)
+            end
 	| Evar (evk,_ as ev), _
             when not (Evar.Set.mem evk flags.frozen_evars) 
 	      && not (occur_evar sigma evk cN) ->
@@ -942,9 +943,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
   and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN =
     try canonical_projections curenvnb pb opt cM cN substn
     with ex when precatchable_exception ex ->
-    let sigma', b = constr_cmp cv_pb env sigma flags cM cN in
-      if b then (sigma', metas, evars)
-      else
+    match constr_cmp cv_pb env sigma flags cM cN with
+    | Some sigma -> (sigma, metas, evars)
+    | None ->
 	try reduce curenvnb pb opt substn cM cN
 	with ex when precatchable_exception ex ->
 	let (f1,l1) =
@@ -1001,12 +1002,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	       (* Renounce, maybe metas/evars prevents typing *) sigma
 	   else sigma
 	 in 
-	 let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in
-	    if b then Some (sigma, metasubst, evarsubst)
-	    else 
-	      if is_ground_term sigma m1 && is_ground_term sigma n1 then
-		error_cannot_unify curenv sigma (cM,cN)
-	      else None
+        match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with
+        | Some sigma ->
+          Some (sigma, metasubst, evarsubst)
+        | None ->
+          if is_ground_term sigma m1 && is_ground_term sigma n1 then
+            error_cannot_unify curenv sigma (cM,cN)
+          else None
     in
       match res with
       | Some substn -> substn
@@ -1109,11 +1111,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
     then
       None
     else 
-      let sigma, b = match flags.modulo_conv_on_closed_terms with
+      let ans = match flags.modulo_conv_on_closed_terms with
 	| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
         | _ -> constr_cmp cv_pb env sigma flags m n in
-	if b then Some sigma
-	else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+      match ans with
+      | Some sigma -> ans
+      | None ->
+        if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
         | Some (cv_id, cv_k), (dl_id, dl_k) ->
           Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
         | None,(dl_id, dl_k) ->
@@ -1603,8 +1607,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
   let merge_fun c1 c2 =
     match c1, c2 with
     | Some (evd,c1,x), Some (_,c2,_) ->
-      let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in
-      if b then Some (evd, c1, x) else raise (NotUnifiable None)
+      begin match infer_conv ~pb:CONV env evd c1 c2 with
+      | Some evd -> Some (evd, c1, x)
+      | None -> raise (NotUnifiable None)
+      end
     | Some _, None -> c1
     | None, Some _ -> c2
     | None, None -> None in
@@ -1921,10 +1927,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
   let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
   let typp = Typing.meta_type evd' p in
   let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
-  let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in
-  if not b then
+  match infer_conv ~pb:CUMUL env evd' predtyp typp with
+  | None ->
     error_wrong_abstraction_type env evd'
       (Evd.meta_name evd p) pred typp predtyp;
+  | Some evd' ->
   w_merge env false flags.merge_unify_flags
           (evd',[p,pred,(Conv,TypeProcessed)],[])
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 218b2671e..95c30d815 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -309,9 +309,10 @@ let check_meta_variables env sigma c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
-      if b then evm 
-      else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
+    let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+    match ans with
+    | Some evm -> evm
+    | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
   else sigma
 
 exception Stop of EConstr.t list
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 58c62af85..d7888f6ca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k =
       let sigma =
         if check then begin
           ignore (Typing.unsafe_type_of env sigma ty);
-          let sigma,b = Reductionops.infer_conv env sigma ty conclty in
-          if not b then error "Not convertible.";
-          sigma
+          match Reductionops.infer_conv env sigma ty conclty with
+          | None -> error "Not convertible."
+          | Some sigma -> sigma
         end else sigma in
       let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
@@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false
 
 let convert_gen pb x y =
   Proofview.Goal.enter begin fun gl ->
-    try
-      let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
-      if b then Proofview.Unsafe.tclEVARS sigma
-      else Tacticals.New.tclFAIL 0 (str "Not convertible")
-    with (* Reduction.NotConvertible *) _ ->
+    match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
+    | Some sigma -> Proofview.Unsafe.tclEVARS sigma
+    | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
+    | exception _ ->
       (** FIXME: Sometimes an anomaly is raised from conversion *)
       Tacticals.New.tclFAIL 0 (str "Not convertible")
 end
@@ -796,15 +795,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
     let t2 = Retyping.get_type_of env sigma origc in
     let sigma, t2 = Evarsolve.refresh_universes
 		      ~onlyalg:true (Some false) env sigma t2 in
-    let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
-    if not b then
+    match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with
+    | None ->
       if
         isSort sigma (whd_all env sigma t1) &&
         isSort sigma (whd_all env sigma t2)
       then (mayneedglobalcheck := true; sigma)
       else
         user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
-    else sigma
+    | Some sigma -> sigma
   end
   else
     if not (isSort sigma (whd_all env sigma t1)) then
@@ -815,9 +814,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
 let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
   let (sigma, t') = t sigma in
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
-  let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
-  if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
-  (sigma, t')
+  match infer_conv ~pb:cv_pb env sigma t' c with
+  | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
+  | Some sigma -> (sigma, t')
 
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb deep t where env sigma c =
@@ -1934,16 +1933,19 @@ let assumption =
     let t = NamedDecl.get_type decl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
-    let (sigma, is_same_type) =
-      if only_eq then (sigma, EConstr.eq_constr sigma t concl)
+    let ans =
+      if only_eq then
+        if EConstr.eq_constr sigma t concl then Some sigma
+        else None
       else
         let env = Proofview.Goal.env gl in
         infer_conv env sigma t concl
     in
-    if is_same_type then
+    match ans with
+    | Some sigma ->
       (Proofview.Unsafe.tclEVARS sigma) <*>
 	exact_no_check (mkVar (NamedDecl.get_id decl))
-    else arec gl only_eq rest
+    | None -> arec gl only_eq rest
   in
   let assumption_tac gl =
     let hyps = Proofview.Goal.hyps gl in
diff --git a/test-suite/Makefile b/test-suite/Makefile
index f41fb5b1e..32e245e36 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -362,26 +362,33 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-	  tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`; \
+	  output=$*.out.real; \
 	  $(call get_command_based_on_flags,"$<") "$<" $(call get_coq_prog_args,"$<") 2>&1 \
 	    | grep -v "Welcome to Coq" \
 	    | grep -v "\[Loading ML file" \
 	    | grep -v "Skipping rcfile loading" \
 	    | grep -v "^<W>" \
 	    | sed 's/File "[^"]*"/File "stdin"/' \
-	    > $$tmpoutput; \
-	  diff -u --strip-trailing-cr $*.out $$tmpoutput 2>&1; R=$$?; times; \
+	    > $$output; \
+	  diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
+	    rm $$output; \
 	  else \
 	    echo $(log_failure); \
 	    echo "    $<...Error! (unexpected output)"; \
 	    $(FAIL); \
 	  fi; \
-	  rm $$tmpoutput; \
 	} > "$@"
 
+.PHONY: approve-output
+approve-output: output
+	$(HIDE)for f in output/*.out.real; do \
+	  mv "$$f" "$${f%.real}"; \
+	  echo "Updated $${f%.real}!"; \
+	done
+
 # the expected output for the MExtraction test is
 # /plugins/micromega/micromega.ml except with additional newline
 output/MExtraction.out: ../plugins/micromega/micromega.ml
diff --git a/test-suite/README.md b/test-suite/README.md
index 4572c98cf..ef2e574ec 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -76,3 +76,17 @@ There are also output tests in `test-suite/output` which consist of a `.v` file
 
 There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
 unit-test framework, as described at http://ounit.forge.ocamlcore.org/.  Use `make unit-tests' in the unit-tests directory to run them.
+
+## Fixing output tests
+
+When an output test `output/foo.v` fails, the output is stored in
+`output/foo.out.real`. Move that file to the reference file
+`output/foo.out` to update the test, approving the new output. Target
+`approve-output` will do this for all failing output tests
+automatically.
+
+Don't forget to check the updated `.out` files into git!
+
+Note that `output/MExtraction.out` is special: it is copied from
+`micromega/micromega.ml` in the plugin source directory. Automatic
+approval will incorrectly update the copy.
diff --git a/test-suite/bugs/closed/7631.v b/test-suite/bugs/closed/7631.v
new file mode 100644
index 000000000..34eb8b867
--- /dev/null
+++ b/test-suite/bugs/closed/7631.v
@@ -0,0 +1,21 @@
+Module NamedContext.
+
+Definition foo := true.
+
+Section Foo.
+
+Let bar := foo.
+
+Eval native_compute in bar.
+
+End Foo.
+
+End NamedContext.
+
+Module RelContext.
+
+Definition foo := true.
+
+Definition bar (x := foo) := Eval native_compute in x.
+
+End RelContext.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index e73312c67..c0b04eb53 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -1,6 +1,5 @@
 The command has indeed failed with message:
-To rename arguments the "rename" flag must be specified.
-Argument A renamed to B.
+Flag "rename" expected to rename A into B.
 File "stdin", line 2, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
 If this is what you want add ': assert' to silence the warning. If you want
@@ -113,5 +112,4 @@ Argument z cannot be declared implicit.
 The command has indeed failed with message:
 Extra arguments: y.
 The command has indeed failed with message:
-To rename arguments the "rename" flag must be specified.
-Argument A renamed to R.
+Flag "rename" expected to rename A into R.
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index c6836a1c7..ed4d69ab0 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -82,7 +82,7 @@ End Retracts.
 (** This lemma is basically a commutation of implication and existential
     quantification:  (EX x | A -> P(x))  <=> (A -> EX x | P(x))
     which is provable in classical logic ( => is already provable in
-    intuitionnistic logic). *)
+    intuitionistic logic). *)
 
 Lemma L1 : forall A B:Prop, retract_cond (pow A) (pow B).
 Proof.
@@ -136,7 +136,7 @@ trivial.
 Qed.
 
 
-Theorem classical_proof_irrelevence : T = F.
+Theorem classical_proof_irrelevance : T = F.
 Proof.
 generalize not_has_fixpoint.
 unfold Not_b.
@@ -148,4 +148,7 @@ intros not_true is_true.
 elim not_true; trivial.
 Qed.
 
+
+Notation classical_proof_irrelevence := classical_proof_irrelevance (compat "8.8").
+
 End Berardis_paradox.
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index dd8149d0a..b6523981c 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -631,8 +631,8 @@ GEXTEND Gram
          t = class_rawexpr ->
           VernacCoercion (CAst.make ~loc:!@loc @@ ByNotation ntn, s, t)
 
-      | IDENT "Context"; c = binders ->
-	  VernacContext c
+      | IDENT "Context"; c = LIST1 binder ->
+          VernacContext (List.flatten c)
 
       | IDENT "Instance"; namesup = instance_name; ":";
 	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9a7f59085..7f6270df1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1131,15 +1131,16 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
   let names = rename prev_names names in
   let renaming_specified = Option.has_some !example_renaming in
 
-  if !rename_flag_required && not rename_flag then
-    user_err ~hdr:"vernac_declare_arguments"
-      (strbrk "To rename arguments the \"rename\" flag must be specified."
-    ++ spc () ++
-       match !example_renaming with
-       | None -> mt ()
-       | Some (o,n) ->
-          str "Argument " ++ Name.print o ++
-            str " renamed to " ++ Name.print n ++ str ".");
+  if !rename_flag_required && not rename_flag then begin
+    let msg =
+      match !example_renaming with
+      | None ->
+        strbrk "To rename arguments the \"rename\" flag must be specified."
+      | Some (o,n) ->
+        strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++
+        strbrk " into " ++ Name.print n ++ str "."
+    in user_err ~hdr:"vernac_declare_arguments" msg
+  end;
 
   let duplicate_names =
     List.duplicates Name.equal (List.filter ((!=) Anonymous) names)