diff --git a/dev/bench/bench.sh b/dev/bench/bench.sh
index 47be3fc4a216..37202ededc15 100755
--- a/dev/bench/bench.sh
+++ b/dev/bench/bench.sh
@@ -98,6 +98,7 @@ export COQ_LOG_DIR=$log_dir
 declare -A auto_overlay_map
 auto_overlay_map[elpi]="rocq-elpi"
 auto_overlay_map[equations]="rocq-equations"
+auto_overlay_map[metarocq]="rocq-metarocq-utils rocq-metarocq-common rocq-metarocq-template rocq-metarocq-pcuic rocq-metarocq-safechecker rocq-metarocq-erasure rocq-metarocq-translations"
 
 if [ "$auto_overlays" ]; then
   CI_PULL_REQUEST="${CI_COMMIT_REF_NAME#pr-}"
diff --git a/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh b/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh
new file mode 100644
index 000000000000..d0bb28df466e
--- /dev/null
+++ b/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh
@@ -0,0 +1,34 @@
+overlay equations https://github.com/SkySkimmer/equations context-secvar 21987
+
+overlay elpi https://github.com/SkySkimmer/coq-elpi context-secvar 21987
+
+#overlay mathcomp https://github.com/SkySkimmer/math-comp context-secvar 21987
+
+#overlay tlc https://github.com/SkySkimmer/tlc context-secvar 21987
+
+overlay kami https://github.com/SkySkimmer/kami context-secvar 21987
+# Make PRs against https://github.com/mit-plv/kami base branch rv32i
+
+overlay metarocq https://github.com/SkySkimmer/metarocq context-secvar 21987
+
+overlay bedrock2 https://github.com/SkySkimmer/bedrock2 context-secvar 21987
+# Make PRs against https://github.com/mit-plv/bedrock2 base branch master
+
+overlay coqutil https://github.com/SkySkimmer/coqutil context-secvar 21987
+# Make PRs against https://github.com/mit-plv/coqutil base branch master
+
+overlay fiat_crypto https://github.com/SkySkimmer/fiat-crypto context-secvar 21987
+
+#overlay ceres https://github.com/SkySkimmer/coq-ceres context-secvar 21987
+
+overlay unicoq https://github.com/SkySkimmer/unicoq context-secvar 21987
+
+overlay mtac2 https://github.com/SkySkimmer/Mtac2 context-secvar 21987
+
+overlay rocq_lsp https://github.com/SkySkimmer/rocq-lsp context-secvar 21987
+
+overlay tactician https://github.com/SkySkimmer/coq-tactician context-secvar 21987
+
+overlay vsrocq https://github.com/SkySkimmer/vsrocq context-secvar 21987
+
+overlay waterproof https://github.com/SkySkimmer/coq-waterproof context-secvar 21987
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e4a2c7717b12..d0a4a803dd77 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -318,7 +318,7 @@ let ppelim_constraints cstrs = pp (Sorts.ElimConstraints.pr qprinter cstrs)
 let ppnamedcontextval e =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  pp (pr_named_context env sigma (named_context_of_val e))
+  pp (pr_named_context_of (Environ.reset_with_named_context e env) sigma)
 
 let ppaucontext auctx =
   let {quals = qnas; univs = unas} = AbstractContext.names auctx in
diff --git a/doc/changelog/04-tactics/21987-context-secvar-Changed.rst b/doc/changelog/04-tactics/21987-context-secvar-Changed.rst
new file mode 100644
index 000000000000..5f8714bf4b94
--- /dev/null
+++ b/doc/changelog/04-tactics/21987-context-secvar-Changed.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  :tacn:`clear` checks that identifiers are bound even when they are ltac variables
+  (typically in `match goal with H : _ |- _ => foo H; clear H end`, `clear` now fails if `foo` cleared H where before it would succeed without doing anything)
+  (`#21987 <https://github.com/rocq-prover/rocq/pull/21987>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst b/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst
new file mode 100644
index 000000000000..58be0ef1c22a
--- /dev/null
+++ b/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst
@@ -0,0 +1,11 @@
+- **Fixed:**
+  the proof engine now keeps track of which hypotheses are section variables
+  instead of assuming that a variable sharing a name with a section variable is a section variable.
+  In particular :tacn:`destruct` now clears non-section-variable variables which share a name with a section variable.
+  Note that modifying a section variable (e.g. with `apply in`) makes it a non-section-variable
+  (`#21987 <https://github.com/rocq-prover/rocq/pull/21987>`_,
+  fixes `#18858 <https://github.com/rocq-prover/rocq/issues/18858>`_
+  and `#12304 <https://github.com/rocq-prover/rocq/issues/12304>`_
+  and `#11487 <https://github.com/rocq-prover/rocq/issues/11487>`_
+  and `#6773 <https://github.com/rocq-prover/rocq/issues/6773>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
index 30c08dee43c5..6fa5f8080d87 100644
--- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
+++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml
@@ -102,8 +102,8 @@ let two_lambda_pattern sigma term =
   function like *)
 let get_type_of_hyp env id =
   match EConstr.lookup_named id env with
-  | Context.Named.Declaration.LocalAssum (_, ty) -> ty
-  | _ -> CErrors.user_err (let open Pp in
+  | LocalAssum (_, ty) -> ty
+  | LocalDef _ -> CErrors.user_err (let open Pp in
                              str (Names.Id.to_string id) ++
                              str " is not a plain hypothesis")
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index f88e0ad5775f..7ea13b8843a0 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1706,6 +1706,14 @@ succeeds, and results in an error otherwise.
    .. exn:: Not a variable or hypothesis.
       :undocumented:
 
+.. tacn:: is_section_var @one_term
+
+   Succeeds if :n:`@one_term` is a section variable in
+   the current local context and fails otherwise.
+
+   .. exn:: Not a section variable.
+      :undocumented:
+
 .. tacn:: is_const @one_term
 
    Succeeds if :n:`@one_term` is a global constant that is neither a (co)inductive
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 762d248d77fe..7b8bfd7f96fb 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1089,6 +1089,12 @@ Controlling display
    after each tactic.  The information is used by the Prooftree tool in Proof
    General. (https://askra.de/software/prooftree)
 
+.. flag:: Printing Variables Status
+
+   This debug :term:`flag` prints whether each variable in the context
+   is a section variable or an hypothesis local to the current proof.
+   It is off by default.
+
 .. extracted from Gallina extensions chapter
 
 .. _printing_constructions_full:
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 38c9d327a6f8..1e2a661598d2 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1826,6 +1826,7 @@ simple_tactic: [
 | "is_evar" constr
 | "has_evar" constr
 | "is_var" constr
+| "is_section_var" constr
 | "is_fix" constr
 | "is_cofix" constr
 | "is_ind" constr
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index d677407a4f1b..bf3fca66453f 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1498,6 +1498,7 @@ simple_tactic: [
 | "is_evar" one_term
 | "has_evar" one_term
 | "is_var" one_term
+| "is_section_var" one_term
 | "is_fix" one_term
 | "is_cofix" one_term
 | "is_ind" one_term
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 60054cd04ddd..52f99c726532 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -171,9 +171,7 @@ type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = (types, ESorts.t) Environ.punsafe_type_judgment
 type named_declaration = (constr, types, ERelevance.t) Context.Named.Declaration.pt
 type rel_declaration = (constr, types, ERelevance.t) Context.Rel.Declaration.pt
-type compacted_declaration = (constr, types, ERelevance.t) Context.Compacted.Declaration.pt
 type named_context = (constr, types, ERelevance.t) Context.Named.pt
-type compacted_context = compacted_declaration list
 type rel_context = (constr, types, ERelevance.t) Context.Rel.pt
 type 'a binder_annot = ('a, ERelevance.t) Context.pbinder_annot
 
@@ -1220,16 +1218,25 @@ let destArity sigma =
 let push_rel d e = push_rel (cast_rel_decl unsafe_eq unsafe_relevance_eq d) e
 let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq unsafe_relevance_eq d) e
 let push_rec_types d e = push_rec_types (cast_rec_decl unsafe_eq unsafe_relevance_eq d) e
-let push_named d e = push_named (cast_named_decl unsafe_eq unsafe_relevance_eq d) e
-let push_named_context d e = push_named_context (cast_named_context unsafe_eq unsafe_relevance_eq d) e
-let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq unsafe_relevance_eq d) e
+let push_named status d e = push_named status (cast_named_decl unsafe_eq unsafe_relevance_eq d) e
+let push_named_context d e =
+  List.fold_right (fun (status, d) env -> push_named status d env) d e
+let push_named_context_val status d e = push_named_context_val status (cast_named_decl unsafe_eq unsafe_relevance_eq d) e
 
 let rel_context e = cast_rel_context (sym unsafe_eq) (sym unsafe_relevance_eq) (rel_context e)
 let named_context e = cast_named_context (sym unsafe_eq) (sym unsafe_relevance_eq) (named_context e)
 
-let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq unsafe_relevance_eq e)
+let val_of_named_context ctxt =
+  List.fold_right (fun (status,d) ctxt -> push_named_context_val status d ctxt)
+    ctxt Environ.empty_named_context_val
+
 let named_context_of_val e = cast_named_context (sym unsafe_eq) (sym unsafe_relevance_eq) (named_context_of_val e)
 
+let named_context_of_val_with_status
+  : named_context_val -> (var_status * named_declaration) list =
+  let Refl, Refl = unsafe_eq, unsafe_relevance_eq in
+  named_context_of_val_with_status
+
 let of_existential : Constr.existential -> existential =
   let gen : type a b. (a,b) eq -> 'c * b SList.t -> 'c * a SList.t = fun Refl x -> x in
   gen unsafe_eq
@@ -1248,10 +1255,28 @@ let map_rel_context_in_env f env sign =
   aux env [] (List.rev sign)
 
 let match_named_context_val :
-  named_context_val -> (named_declaration * named_context_val) option =
+  named_context_val -> (var_status * named_declaration * named_context_val) option =
   match unsafe_eq, unsafe_relevance_eq with
   | Refl, Refl -> match_named_context_val
 
+let fold_named_context_val :
+  (named_context_val -> var_status -> named_declaration -> 'a -> 'a) ->
+  named_context_val -> init:'a -> 'a =
+  let Refl, Refl = unsafe_eq, unsafe_relevance_eq in
+  Environ.fold_named_context_val
+
+let fold_named_context :
+  (env -> var_status -> named_declaration -> 'a -> 'a) ->
+  env -> init:'a -> 'a =
+  let Refl, Refl = unsafe_eq, unsafe_relevance_eq in
+  Environ.fold_named_context
+
+let map_named_val :
+  (var_status -> named_declaration -> var_status * named_declaration) ->
+  named_context_val -> named_context_val =
+  match unsafe_eq, unsafe_relevance_eq with
+  | Refl, Refl -> map_named_val
+
 let identity_subst_val : named_context_val -> t SList.t = fun ctx ->
   SList.defaultn (List.length ctx.Environ.env_named_ctx) SList.empty
 
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 861bdf094d96..7ee9a48ce89f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -93,9 +93,7 @@ type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = (types, Evd.esorts) Environ.punsafe_type_judgment
 type named_declaration = (constr, types, ERelevance.t) Context.Named.Declaration.pt
 type rel_declaration = (constr, types, ERelevance.t) Context.Rel.Declaration.pt
-type compacted_declaration = (constr, types, ERelevance.t) Context.Compacted.Declaration.pt
 type named_context = (constr, types, ERelevance.t) Context.Named.pt
-type compacted_context = compacted_declaration list
 type rel_context = (constr, types, ERelevance.t) Context.Rel.pt
 type 'a binder_annot = ('a,ERelevance.t) Context.pbinder_annot
 
@@ -424,15 +422,24 @@ val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
 val push_rec_types : rec_declaration -> env -> env
 
-val push_named : named_declaration -> env -> env
-val push_named_context : named_context -> env -> env
-val push_named_context_val  : named_declaration -> named_context_val -> named_context_val
+val push_named : var_status -> named_declaration -> env -> env
+val push_named_context : (var_status * named_declaration) list -> env -> env
+val push_named_context_val  : var_status -> named_declaration -> named_context_val -> named_context_val
 
 val rel_context : env -> rel_context
 val named_context : env -> named_context
 
-val val_of_named_context : named_context -> named_context_val
+val val_of_named_context : (var_status * named_declaration) list -> named_context_val
 val named_context_of_val : named_context_val -> named_context
+val named_context_of_val_with_status : named_context_val -> (var_status * named_declaration) list
+
+val fold_named_context_val :
+  (named_context_val -> var_status -> named_declaration -> 'a -> 'a) ->
+  named_context_val -> init:'a -> 'a
+
+val fold_named_context :
+  (env -> var_status -> named_declaration -> 'a -> 'a) ->
+  env -> init:'a -> 'a
 
 val lookup_rel : int -> env -> rel_declaration
 val lookup_named : variable -> env -> named_declaration
@@ -445,7 +452,14 @@ val map_rel_context_in_env :
   (env -> constr -> constr) -> env -> rel_context -> rel_context
 
 val match_named_context_val :
-  named_context_val -> (named_declaration * named_context_val) option
+  named_context_val -> (var_status * named_declaration * named_context_val) option
+
+(** [map_named_val f ctxt] apply [f] to the body and the type of
+   each declarations.
+   *** /!\ ***   [f t] must preserve the name *)
+val map_named_val :
+  (var_status -> named_declaration -> var_status * named_declaration) ->
+  named_context_val -> named_context_val
 
 val identity_subst_val : named_context_val -> t SList.t
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 438e23bd16b5..7adf698fc061 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -63,17 +63,17 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
 let nf_relevance sigma r =
   UState.nf_relevance (Evd.ustate sigma) r
 
-let nf_named_context_evar sigma ctx =
-  Context.Named.map_with_relevance (nf_relevance sigma) (nf_evars_universes sigma) ctx
+let nf_named_decl_evar sigma status ctx =
+  status, Context.Named.Declaration.map_constr_with_relevance (nf_relevance sigma) (nf_evars_universes sigma) ctx
 
 let nf_rel_context_evar sigma ctx =
   let nf_relevance r = ERelevance.make (ERelevance.kind sigma r) in
   Context.Rel.map_with_relevance nf_relevance (nf_evar sigma) ctx
 
 let nf_env_evar sigma env =
-  let nc' = nf_named_context_evar sigma (Environ.named_context env) in
+  let nc' = Environ.map_named_val (nf_named_decl_evar sigma) (Environ.named_context_val env) in
   let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in
-    EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
+    EConstr.push_rel_context rel' (reset_with_named_context nc' env)
 
 let nf_evar_info evc info = map_evar_info (nf_evar evc) info
 
@@ -114,6 +114,7 @@ let is_ground_env evd env =
     | RelDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
     | _ -> true in
   let is_ground_named_decl = function
+    (* skip if SecVar? *)
     | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b)
     | _ -> true in
   List.for_all is_ground_rel_decl (rel_context env) &&
@@ -283,18 +284,7 @@ let update_var src tgt subst =
       let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in
       { subst with csubst_var; csubst_rev }
 
-module VarSet =
-struct
-  type t = Id.t -> bool
-  let empty _ = false
-  let full _ = true
-  let variables env id = is_section_variable env id
-end
-
-type naming_mode = VarSet.t
-
 let push_rel_decl_to_named_context
-  ~hypnaming
   sigma decl (ext : ext_named_context) =
   let open EConstr in
   let open Vars in
@@ -303,14 +293,15 @@ let push_rel_decl_to_named_context
   in
   let rec replace_var_named_declaration id0 id nc = match match_named_context_val nc with
   | None -> empty_named_context_val
-  | Some (decl, nc) ->
+  | Some (status, decl, nc) ->
     if Id.equal id0 (NamedDecl.get_id decl) then
-      (* Stop here, the variable cannot occur before its definition *)
-      push_named_context_val (NamedDecl.set_id id decl) nc
+      (* Stop here, the variable cannot occur before its definition
+         NB: we lose section variable status *)
+      push_named_context_val ProofVar (NamedDecl.set_id id decl) nc
     else
       let nc = replace_var_named_declaration id0 id nc in
       let vsubst = [id0 , mkVar id] in
-      push_named_context_val (map_decl (fun c -> replace_vars sigma vsubst c) decl) nc
+      push_named_context_val status (map_decl (fun c -> replace_vars sigma vsubst c) decl) nc
   in
   let extract_if_neq id = function
     | Anonymous -> None
@@ -325,7 +316,7 @@ let push_rel_decl_to_named_context
   in
   match extract_if_neq id na with
   | Some id0 ->
-    if hypnaming id0 then
+    if Id.Map.mem id0 ext.ext_ctx.env_named_map && is_section_variable_sign ext.ext_ctx id0 then
       (* spiwack: if [id0] is a section variable renaming it is
           incorrect. We revert to a less robust behaviour where
           the new binder has name [id]. Which amounts to the same
@@ -333,7 +324,7 @@ let push_rel_decl_to_named_context
       let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst sigma ext.ext_subst) in
       { ext_subst = push_var id ext.ext_subst;
         ext_avoid = Id.Set.add id ext.ext_avoid;
-        ext_ctx = push_named_context_val d ext.ext_ctx }
+        ext_ctx = push_named_context_val ProofVar d ext.ext_ctx }
     else
       (* spiwack: if [id<>id0], rather than introducing a new
           binding named [id], we will keep [id0] (the name given
@@ -345,12 +336,12 @@ let push_rel_decl_to_named_context
       let avoid = Id.Set.add id (Id.Set.add id0 ext.ext_avoid) in
       { ext_subst = push_var id0 subst;
         ext_avoid = avoid;
-        ext_ctx = push_named_context_val d nc }
+        ext_ctx = push_named_context_val ProofVar d nc }
   | None ->
     let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst sigma ext.ext_subst) in
     { ext_subst = push_var id ext.ext_subst;
       ext_avoid = Id.Set.add id ext.ext_avoid;
-      ext_ctx = push_named_context_val d ext.ext_ctx }
+      ext_ctx = push_named_context_val ProofVar d ext.ext_ctx }
 
 let csubst_instance subst ctx =
   let fold decl accu = match Id.Map.find (NamedDecl.get_id decl) subst.csubst_rev with
@@ -368,7 +359,7 @@ let ext_rev_subst { ext_subst = subst } id0 =
 let default_ext_instance { ext_subst = subst; ext_ctx = ctx } =
   csubst_instance subst (named_context_of_val ctx)
 
-let push_rel_context_to_named_context ~hypnaming env sigma typ =
+let push_rel_context_to_named_context env sigma typ =
   (* compute the instances relative to the named context and rel_context *)
   let open EConstr in
   let ctx = named_context_val env in
@@ -382,15 +373,15 @@ let push_rel_context_to_named_context ~hypnaming env sigma typ =
     (* We do keep the instances corresponding to local definition (see above) *)
     let init = { ext_subst = empty_csubst; ext_avoid = avoid; ext_ctx = ctx } in
     let ext =
-      Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
+      Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
         (rel_context env) ~init in
     let inst = default_ext_instance ext in
     (ext.ext_ctx, csubst_subst sigma ext.ext_subst typ, inst, ext.ext_subst)
 
-let ext_named_context_of_env ~hypnaming env sigma =
+let ext_named_context_of_env env sigma =
   let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
   let init = { ext_subst = empty_csubst; ext_avoid = avoid; ext_ctx = named_context_val env } in
-  Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
+  Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
     (EConstr.rel_context env) ~init
 
 (*------------------------------------*
@@ -407,13 +398,9 @@ let next_evar_name naming = match naming with
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 let new_evar ?src ?filter ?relevance ?abstract_arguments ?candidates ?(naming = IntroAnonymous) ?parent ?typeclass_candidate
-    ?rrpat ?hypnaming env evd typ =
+    ?rrpat env evd typ =
   let name = next_evar_name naming in
-  let hypnaming = match hypnaming with
-  | Some n -> n
-  | None -> VarSet.variables (Global.env ())
-  in
-  let sign,typ',instance,subst = push_rel_context_to_named_context ~hypnaming env evd typ in
+  let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in
   let map c = csubst_subst evd subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
   let instance =
@@ -428,10 +415,10 @@ let new_evar ?src ?filter ?relevance ?abstract_arguments ?candidates ?(naming =
     ?typeclass_candidate in
   (evd, EConstr.mkEvar (evk, instance))
 
-let new_type_evar ?src ?filter ?naming ?hypnaming env evd rigid =
+let new_type_evar ?src ?filter ?naming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
   let relevance = EConstr.ESorts.relevance_of_sort s in
-  let (evd', e) = new_evar env evd' ?src ?filter ~relevance ?naming ~typeclass_candidate:false ?hypnaming (EConstr.mkSort s) in
+  let (evd', e) = new_evar env evd' ?src ?filter ~relevance ?naming ~typeclass_candidate:false (EConstr.mkSort s) in
   evd', (e, s)
 
 let new_Type ?(rigid=Evd.univ_flexible) evd =
@@ -516,7 +503,7 @@ let check_vars env sigma ids c =
   in
   check_rec c
 
-let rec check_and_clear_in_constr ~is_section_variable env evdref err ids ~global c =
+let rec check_and_clear_in_constr env evdref err ids ~global c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
      evars). [global] should be true iff there is some variable of [ids] which
@@ -583,9 +570,10 @@ let rec check_and_clear_in_constr ~is_section_variable env evdref err ids ~globa
               let _nconcl : EConstr.t =
                 try
                   let nids = Id.Map.domain rids in
-                  let global = Id.Set.exists is_section_variable nids in
+                  let env = evar_filtered_env env evi in
+                  let global = Id.Set.exists (is_section_variable_env env) nids in
                   let concl = evar_concl evi in
-                  check_and_clear_in_constr ~is_section_variable env evdref (EvarTypingBreak ev) nids ~global concl
+                  check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids ~global concl
                 with ClearDependencyError (rid,err,where) ->
                   raise (ClearDependencyError (Id.Map.find rid rids,err,where))
               in
@@ -597,22 +585,21 @@ let rec check_and_clear_in_constr ~is_section_variable env evdref err ids ~globa
               evdref := evd;
               Evd.existential_value !evdref ev
 
-      | _ -> EConstr.map !evdref (check_and_clear_in_constr ~is_section_variable env evdref err ids ~global) c
+      | _ -> EConstr.map !evdref (check_and_clear_in_constr env evdref err ids ~global) c
 
 let clear_hyps_in_evi_main env sigma hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occurring in evi *)
   let evdref = ref sigma in
-  let is_section_variable id = is_section_variable (Global.env ()) id in
-  let global = Id.Set.exists is_section_variable ids in
+  let global = Id.Set.exists (is_section_variable_env env) ids in
   let terms =
-    List.map (check_and_clear_in_constr ~is_section_variable env evdref (OccurHypInSimpleClause None) ids ~global) terms in
+    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids ~global) terms in
   let nhyps =
-    let check_context decl =
+    let check_context status decl =
       let decl = EConstr.of_named_decl decl in
       let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in
-      EConstr.Unsafe.to_named_decl @@ NamedDecl.map_constr (check_and_clear_in_constr ~is_section_variable env evdref err ids ~global) decl
+      status, EConstr.Unsafe.to_named_decl @@ NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids ~global) decl
     in
     remove_hyps ids check_context hyps
   in
@@ -620,8 +607,9 @@ let clear_hyps_in_evi_main env sigma hyps terms ids =
 
 let check_and_clear_in_constr env evd err ids c =
   let evdref = ref evd in
+  let global = Id.Set.exists (is_section_variable_env env) ids in
   let _ : EConstr.constr = check_and_clear_in_constr
-      ~is_section_variable:(fun _ -> true) ~global:true
+      ~global
       env evdref err ids c
   in
   !evdref
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index dcd6036b5b1c..b942316b5294 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -26,16 +26,6 @@ val new_meta : unit -> metavariable
 
 val next_evar_name : intro_pattern_naming_expr -> (Id.t * bool) option
 
-module VarSet :
-sig
-  type t
-  val empty : t
-  val full : t
-  val variables : Environ.env -> t
-end
-
-type naming_mode = VarSet.t
-
 val new_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?relevance:ERelevance.t ->
@@ -44,7 +34,6 @@ val new_evar :
   ?parent:Evar.t ->
   ?typeclass_candidate:bool ->
   ?rrpat:bool ->
-  ?hypnaming:naming_mode ->
   env -> evar_map -> types -> evar_map * EConstr.t
 
 (** Alias of {!Evd.new_pure_evar} *)
@@ -63,7 +52,6 @@ val new_pure_evar :
 val new_type_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?naming:intro_pattern_naming_expr ->
-  ?hypnaming:naming_mode ->
   env -> evar_map -> rigid ->
   evar_map * (constr * ESorts.t)
 
@@ -128,7 +116,6 @@ val jv_nf_evar :
 val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context
 val nf_rel_context_evar : evar_map -> rel_context -> rel_context
 val nf_env_evar : evar_map -> env -> env
 
@@ -199,6 +186,8 @@ type unification_pb = conv_pb * env * constr * constr
     Put it at the end of the list if [tail] is true, by default it is false. *)
 val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map
 
+val vars_of_global : env -> evar_map -> GlobRef.t -> Id.Set.t
+
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
@@ -238,7 +227,7 @@ val csubst_subst : Evd.evar_map -> csubst -> constr -> constr
 
 type ext_named_context
 
-val ext_named_context_of_env : hypnaming:naming_mode -> env -> evar_map -> ext_named_context
+val ext_named_context_of_env : env -> evar_map -> ext_named_context
 
 val ext_named_context_val : ext_named_context -> named_context_val
 val ext_csubst : ext_named_context -> csubst
@@ -247,10 +236,10 @@ val default_ext_instance : ext_named_context -> constr SList.t
 
 val ext_rev_subst : ext_named_context -> Id.t -> constr
 
-val push_rel_decl_to_named_context : hypnaming:naming_mode ->
+val push_rel_decl_to_named_context :
   evar_map -> rel_declaration -> ext_named_context -> ext_named_context
 
-val push_rel_context_to_named_context : hypnaming:naming_mode ->
+val push_rel_context_to_named_context :
   Environ.env -> evar_map -> types ->
   named_context_val * types * constr SList.t * csubst
 
diff --git a/engine/evd.ml b/engine/evd.ml
index 8a79608a92a9..87f913f0dfc9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -257,15 +257,15 @@ let evar_hyps evi = evi.evar_hyps
 let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with
 | None -> evar_hyps evi
 | Some filter ->
-  let rec make_hyps filter ctxt = match filter, ctxt with
-  | [], [] -> empty_named_context_val
-  | false :: filter, _ :: ctxt -> make_hyps filter ctxt
-  | true :: filter, decl :: ctxt ->
+  let rec make_hyps filter ctxt = match filter, match_named_context_val ctxt with
+  | [], None -> empty_named_context_val
+  | false :: filter, Some (_, _,  ctxt) -> make_hyps filter ctxt
+  | true :: filter, Some (status, decl, ctxt) ->
     let hyps = make_hyps filter ctxt in
-    push_named_context_val decl hyps
+    push_named_context_val status decl hyps
   | _ -> instance_mismatch ()
   in
-  make_hyps filter (evar_context evi)
+  make_hyps filter (evar_hyps evi)
 
 let evar_env env evi =
   Environ.reset_with_named_context evi.evar_hyps env
@@ -290,7 +290,7 @@ let map_when_undefined (type a b) f : (a, b) when_undefined -> (a, b) when_undef
 let map_evar_info f evi =
   {evi with
     evar_body = map_evar_body f evi.evar_body;
-    evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps;
+    evar_hyps = map_named_val (fun status d -> status, NamedDecl.map_constr f d) evi.evar_hyps;
     evar_concl = map_when_undefined f evi.evar_concl;
     evar_candidates = map_when_undefined (fun c -> Option.map (List.map f) c) evi.evar_candidates }
 
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 5494bc998e47..524adcc47d1c 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -99,10 +99,6 @@ let is_constructor id =
   with Not_found ->
     false
 
-let is_section_variable env id =
-  try let _ = Environ.lookup_named id env in true
-  with Not_found -> false
-
 (**********************************************************************)
 (* Generating "intuitive" names from its type *)
 
@@ -401,7 +397,7 @@ let next_name_away_in_cases_pattern gen sigma env_t na avoid =
 
 let next_ident_away_in_goal env id avoid =
   let id = if Id.Set.mem id avoid then restart_subscript id else id in
-  let bad id = Id.Set.mem id avoid || (is_global id && not (is_section_variable env id)) in
+  let bad id = Id.Set.mem id avoid || (is_global id && not (Environ.mem_named id env)) in
   next_ident_away_from id bad
 
 let next_name_away_in_goal (type a) (gen : a Generator.t) env na (avoid : a) =
@@ -409,7 +405,7 @@ let next_name_away_in_goal (type a) (gen : a Generator.t) env na (avoid : a) =
     | Name id -> id
     | Anonymous -> default_non_dependent_ident in
   let id = if Generator.is_fresh gen id avoid then id else restart_subscript id in
-  let bad id = is_global id && not (is_section_variable env id) in
+  let bad id = is_global id && not (Environ.mem_named id env) in
   Generator.gen_ident ~filter:bad gen id avoid
 
 (* 3- Looks for next fresh name outside a list that is moreover valid
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 10e28d719656..60e00a223312 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -41,7 +41,7 @@ let proofview p =
 let compact el ({ solution } as pv) =
   let nf c = Evarutil.nf_evar solution c in
   let nf0 c = EConstr.(to_constr ~abort_on_undefined_evars:false solution (of_constr c)) in
-  let nf_hyps hyps = Environ.map_named_val (fun d -> map_constr nf0 d) hyps in
+  let nf_hyps hyps = Environ.map_named_val (fun status d -> status, map_constr nf0 d) hyps in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (hyps,t,ty) -> nf_hyps hyps, nf t, nf ty) el in
   let pruned_solution = Evd.drop_all_defined solution in
@@ -916,15 +916,19 @@ module Progress = struct
   let eq_named_context_val sigma1 sigma2 ctx1 ctx2 =
     let r_eq _ _ = true (* ignore relevances *) in
     let c1 = EConstr.named_context_of_val ctx1 and c2 = EConstr.named_context_of_val ctx2 in
+    (* should we check variable status? if x is secvar,
+       [rename x into x'; rename x' into x] loses the secvar status
+       so maybe should progress?
+       NB Don't forget to also change the fast path if we change this *)
     let eq_named_declaration d1 d2 =
       match d1, d2 with
       | LocalAssum (i1,t1), LocalAssum (i2,t2) ->
-         Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 t1 t2
+        Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 t1 t2
       | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) ->
-         Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 c1 c2
-         && eq_constr sigma1 sigma2 t1 t2
+        Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 c1 c2 &&
+        eq_constr sigma1 sigma2 t1 t2
       | _ ->
-         false
+        false
     in
     (* NB: can't use List.equal because it shortcuts on physical equality *)
     List.for_all2eq eq_named_declaration c1 c2
@@ -960,9 +964,11 @@ module Progress = struct
     let c1 = EConstr.named_context_of_val ctx1 in
     let c2 = EConstr.named_context_of_val ctx2 in
     let eq_named_declaration d1 d2 = match d1, d2 with
-    | LocalAssum (i1, _), LocalAssum (i2, _) -> Context.eq_annot Names.Id.equal r_eq i1 i2
-    | LocalDef (i1, _, _), LocalDef (i2, _, _) -> Context.eq_annot Names.Id.equal r_eq i1 i2
-    | _ -> false
+      | LocalAssum (i1, _), LocalAssum (i2, _) ->
+        Context.eq_annot Names.Id.equal r_eq i1 i2
+      | LocalDef (i1, _, _), LocalDef (i2, _, _) ->
+        Context.eq_annot Names.Id.equal r_eq i1 i2
+      | _ -> false
     in
     List.for_all2eq eq_named_declaration c1 c2
 
diff --git a/engine/termops.ml b/engine/termops.ml
index 660e57c349df..70659d9389da 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -22,7 +22,6 @@ open Environ
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
-module CompactedDecl = Context.Compacted.Declaration
 
 module Internal = struct
 
@@ -62,7 +61,7 @@ module Internal = struct
 
   let print_named_context env sigma =
     hv 0 (fold_named_context
-            (fun env d pps ->
+            (fun env _status d pps ->
                pps ++ ws 2 ++ pr_var_decl env sigma d)
             env ~init:(mt ()))
 
@@ -74,7 +73,7 @@ module Internal = struct
   let print_env env sigma =
     let sign_env =
       fold_named_context
-        (fun env d pps ->
+        (fun env _status d pps ->
            let pidt =  pr_var_decl env sigma d in
            (pps ++ fnl () ++ pidt))
         env ~init:(mt ())
@@ -149,9 +148,11 @@ let pr_decl env sigma (decl,ok) =
   let open NamedDecl in
   let print_constr = Internal.print_kconstr in
   match decl with
-  | LocalAssum ({binder_name=id},_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}")
-  | LocalDef ({binder_name=id},c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++
-                           print_constr env sigma c ++ str (if ok then ")" else "}")
+  | LocalAssum ({binder_name=id},_) ->
+    if ok then Id.print id else (str "{" ++ Id.print id ++ str "}")
+  | LocalDef ({binder_name=id},c,_) ->
+    str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++
+    print_constr env sigma c ++ str (if ok then ")" else "}")
 
 let pr_evar_source env sigma = function
   | Evar_kinds.NamedHole id -> Id.print id
@@ -877,10 +878,7 @@ let dependent sigma c t = dependent_main false sigma c t
 let dependent_no_evar sigma c t = dependent_main true sigma c t
 
 let dependent_in_decl sigma a decl =
-  let open NamedDecl in
-  match decl with
-    | LocalAssum (_,t) -> dependent sigma a t
-    | LocalDef (_, body, t) -> dependent sigma a body || dependent sigma a t
+  NamedDecl.exists (dependent sigma a) decl
 
 let count_occurrences sigma m t =
   let open EConstr in
@@ -1008,9 +1006,13 @@ let ids_of_context env =
 let names_of_rel_context env =
   List.map RelDecl.get_name (rel_context env)
 
-let is_section_variable env id =
-  try let _ = Environ.lookup_named id env in true
-  with Not_found -> false
+let is_section_variable_sign ?check sign id =
+  match Environ.var_status_ctxt ?check id sign with
+  | SecVar -> true
+  | ProofVar -> false
+
+let is_section_variable_env ?check env id =
+  is_section_variable_sign ?check (Environ.named_context_val env) id
 
 let is_template_polymorphic_ref env sigma f =
   match EConstr.kind sigma f with
@@ -1179,33 +1181,11 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 let mem_named_context_val id ctxt =
   try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false
 
-let compact_named_context sigma sign =
-  let compact l decl =
-    match decl, l with
-    | NamedDecl.LocalAssum (i,t), [] ->
-       [CompactedDecl.LocalAssum ([i],t)]
-    | NamedDecl.LocalDef (i,c,t), [] ->
-       [CompactedDecl.LocalDef ([i],c,t)]
-    | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q ->
-       if EConstr.eq_constr sigma t1 t2
-       then CompactedDecl.LocalAssum (i1::li, t2) :: q
-       else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q
-    | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q ->
-       if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2
-       then CompactedDecl.LocalDef (i1::li, c2, t2) :: q
-       else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q
-    | NamedDecl.LocalAssum (i,t), q ->
-       CompactedDecl.LocalAssum ([i],t) :: q
-    | NamedDecl.LocalDef (i,c,t), q ->
-       CompactedDecl.LocalDef ([i],c,t) :: q
-  in
-  sign |> Context.Named.fold_inside compact ~init:[] |> List.rev
-
 let clear_named_body id env =
   let open NamedDecl in
-  let aux _ = function
-  | LocalDef (id',c,t) when Id.equal id id'.binder_name -> push_named (LocalAssum (id',t))
-  | d -> push_named d in
+  let aux _ status = function
+  | LocalDef (id',c,t) when Id.equal id id'.binder_name -> push_named status (LocalAssum (id',t))
+  | d -> push_named status d in
   fold_named_context aux env ~init:(reset_context env)
 
 let global_vars_set env sigma constr =
@@ -1424,3 +1404,8 @@ and hash_branches bl =
   Array.fold_left (fun acc t -> combine acc (hash_under_context t)) 0 bl
 
 end
+
+(* deprecated *)
+let is_section_variable env id =
+  try let _ = Environ.lookup_named id env in true
+  with Not_found -> false
diff --git a/engine/termops.mli b/engine/termops.mli
index 7a107183fd72..167713da5211 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -194,7 +194,6 @@ val fold_named_context_both_sides :
   ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) ->
     Constr.named_context -> init:'a -> 'a
 val mem_named_context_val : Id.t -> named_context_val -> bool
-val compact_named_context : Evd.evar_map -> EConstr.named_context -> EConstr.compacted_context
 
 val clear_named_body : Id.t -> env -> env
 
@@ -206,8 +205,15 @@ val global_app_of_constr : Evd.evar_map -> constr -> (GlobRef.t * EInstance.t) *
    containing a given set *)
 val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.t list
 
-(** Test if an identifier is the basename of a global reference *)
+(** This tests if the ident is known in the given env, intended to be used with the global env. *)
 val is_section_variable : env -> Id.t -> bool
+[@@deprecated "Use is_section_variable_env on the local env instead of is_section_variable on the global env."]
+
+(** Check if the ident has [SecVar] status in this enviroment.
+    By default [check=true] and produce anomaly if it is not bound.
+    If [check=false] returns [false] if it is not bound. *)
+val is_section_variable_sign : ?check:bool -> Environ.named_context_val -> Id.t -> bool
+val is_section_variable_env : ?check:bool -> env -> Id.t -> bool
 
 val is_template_polymorphic_ref : env -> Evd.evar_map -> constr -> bool
 val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool
diff --git a/ide/rocqide/idetop.ml b/ide/rocqide/idetop.ml
index 0336f939ceba..7afdb18ea3d9 100644
--- a/ide/rocqide/idetop.ml
+++ b/ide/rocqide/idetop.ml
@@ -207,7 +207,7 @@ let process_goal short sigma g =
     if short then [] else
       let hyps =
         List.rev_map process_hyp
-        (Termops.compact_named_context sigma (EConstr.named_context env))
+          (Ppconstr.compact_named_context sigma (Environ.named_context_val env))
       in
       hyps
   in
@@ -301,7 +301,7 @@ let hints () =
     | [] -> None
     | g :: _ ->
       let env = Evd.evar_filtered_env (Global.env ()) (Evd.find_undefined sigma g) in
-      let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
+      let get_hint_hyp env _ d accu = hyp_next_tac sigma env d :: accu in
       let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
       Some (hint_hyps, concl_next_tac)
   with Vernacstate.Declare.NoCurrentProof -> None
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 35ff54ca4669..3696fb418ac1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -3110,7 +3110,7 @@ let interp_context_evars_gen ?(program_mode=false) ?(unconstrained_sorts = false
 let interp_named_context_evars ?program_mode ?unconstrained_sorts ?poly ?impl_env ?autoimp_enable env sigma bl =
   let extract_name ?loc = function Name id -> id | Anonymous -> user_err ?loc Pp.(str "Unexpected anonymous variable.") in
   let make_decl ?loc = Context.Named.Declaration.of_rel_decl (extract_name ?loc) in
-  interp_context_evars_gen ?program_mode ?unconstrained_sorts ?poly ?impl_env ?autoimp_enable ~dump:false env sigma make_decl EConstr.push_named bl
+  interp_context_evars_gen ?program_mode ?unconstrained_sorts ?poly ?impl_env ?autoimp_enable ~dump:false env sigma make_decl (EConstr.push_named ProofVar) bl
 
 let interp_context_evars ?program_mode ?unconstrained_sorts ?poly ?impl_env env sigma bl =
   interp_context_evars_gen ?program_mode ?unconstrained_sorts ?poly ?impl_env ~autoimp_enable:false ~dump:true env sigma (fun ?loc d -> d) EConstr.push_rel bl
diff --git a/kernel/constr.ml b/kernel/constr.ml
index a05c35c581e6..e7051c6e4af6 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1383,10 +1383,8 @@ let hcons = HCons.hcons
 
 type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt
 type named_declaration = (constr, types, Sorts.relevance) Context.Named.Declaration.pt
-type compacted_declaration = (constr, types, Sorts.relevance) Context.Compacted.Declaration.pt
 type rel_context = rel_declaration list
 type named_context = named_declaration list
-type compacted_context = compacted_declaration list
 
 (** Minimalistic constr printer, typically for debugging *)
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index c578e1d29798..edb0d9fe3cc8 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -430,10 +430,8 @@ val eq_constr_nounivs : constr -> constr -> bool
 
 type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt
 type named_declaration = (constr, types, Sorts.relevance) Context.Named.Declaration.pt
-type compacted_declaration = (constr, types, Sorts.relevance) Context.Compacted.Declaration.pt
 type rel_context = rel_declaration list
 type named_context = named_declaration list
-type compacted_context = compacted_declaration list
 
 (** {6 Relocation and substitution } *)
 
diff --git a/kernel/context.ml b/kernel/context.ml
index dbcdd89eb593..a0d9f84432eb 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -569,32 +569,3 @@ struct
   let instance mk l =
     Array.of_list (instance_list mk l)
 end
-
-module Compacted =
-  struct
-    module Declaration =
-      struct
-        type ('constr, 'types, 'r) pt =
-          | LocalAssum of (Id.t,'r) pbinder_annot list * 'types
-          | LocalDef of (Id.t,'r) pbinder_annot list * 'constr * 'types
-
-        let map_constr f = function
-          | LocalAssum (ids, ty) as decl ->
-             let ty' = f ty in
-             if ty == ty' then decl else LocalAssum (ids, ty')
-          | LocalDef (ids, c, ty) as decl ->
-             let ty' = f ty in
-             let c' = f c in
-             if c == c' && ty == ty' then decl else LocalDef (ids,c',ty')
-
-        let of_named_decl = function
-          | Named.Declaration.LocalAssum (id,t) ->
-              LocalAssum ([id],t)
-          | Named.Declaration.LocalDef (id,v,t) ->
-              LocalDef ([id],v,t)
-      end
-
-    type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list
-
-    let fold f l ~init = List.fold_right f l init
-  end
diff --git a/kernel/context.mli b/kernel/context.mli
index e8d2e0e1d1b3..7d67681980ce 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -370,20 +370,3 @@ sig
   (** [instance_list] is like [instance] but returning a list. *)
   val instance_list : (Id.t -> 'v) -> ('c, 't, 'r) pt -> 'v list
 end
-
-module Compacted :
-sig
-  module Declaration :
-  sig
-    type ('constr, 'types, 'r) pt =
-      | LocalAssum of (Id.t,'r) pbinder_annot list * 'types
-      | LocalDef of (Id.t,'r) pbinder_annot list * 'constr * 'types
-
-    val map_constr : ('c -> 'c) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt
-    val of_named_decl : ('c, 't, 'r) Named.Declaration.pt -> ('c, 't, 'r) pt
-  end
-
-  type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list
-
-  val fold : (('c, 't, 'r) Declaration.pt -> 'a -> 'a) -> ('c, 't, 'r) pt -> init:'a -> 'a
-end
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 54d4ded25492..7f5295a5e76a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -80,6 +80,7 @@ type named_context_val = {
   env_named_ctx : Constr.named_context;
   env_named_map : Constr.named_declaration Id.Map.t;
   env_named_idx : Constr.named_declaration Range.t;
+  env_named_secvars : Id.Set.t;
 }
 
 type rel_context_val = {
@@ -118,6 +119,7 @@ let empty_named_context_val = {
   env_named_ctx = [];
   env_named_map = Id.Map.empty;
   env_named_idx = Range.empty;
+  env_named_secvars = Id.Set.empty;
 }
 
 let empty_rel_context_val = {
@@ -187,43 +189,85 @@ let set_rel_context_val v env =
     env_nb_rel = Range.length v.env_rel_map; }
 
 (* Named context *)
-
-let push_named_context_val d ctxt =
-(*   assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *)
+type var_status = SecVar | ProofVar
+
+let var_status_eq a b = match a, b with
+  | SecVar, SecVar -> true
+  | ProofVar, ProofVar -> true
+  | (SecVar | ProofVar), _ -> false
+
+let push_named_context_val status d ctxt =
+  let id = NamedDecl.get_id d in
+  (* we would like the stronger assert but it breaks in bug_4095 *)
+  (* assert (not (Id.Map.mem id ctxt.env_named_map)); *)
+  assert (not (Id.Set.mem id ctxt.env_named_secvars));
+  let secvars = match status with
+    | ProofVar -> ctxt.env_named_secvars
+    | SecVar -> Id.Set.add id ctxt.env_named_secvars
+  in
   {
     env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
-    env_named_map = Id.Map.add (NamedDecl.get_id d) d ctxt.env_named_map;
+    env_named_map = Id.Map.add id d ctxt.env_named_map;
     env_named_idx = Range.cons d ctxt.env_named_idx;
+    env_named_secvars = secvars;
   }
 
+let var_status_ctxt ?(check=true) id ctxt =
+  if Id.Set.mem id ctxt.env_named_secvars then SecVar
+  else
+    let () = assert (not check || Id.Map.mem id ctxt.env_named_map) in
+    ProofVar
+
+let var_status ?check id env = var_status_ctxt ?check id env.env_named_context
+
 let match_named_context_val c = match c.env_named_ctx with
 | [] -> None
 | decl :: ctx ->
-  let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in
-  let cval = { env_named_ctx = ctx; env_named_map = map; env_named_idx = Range.tl c.env_named_idx } in
-  Some (decl, cval)
+  let id = NamedDecl.get_id decl in
+  let map = Id.Map.remove id c.env_named_map in
+  let secvars = Id.Set.remove id c.env_named_secvars in
+  let status = if secvars == c.env_named_secvars then ProofVar else SecVar in
+  let cval = {
+    env_named_ctx = ctx;
+    env_named_map = map;
+    env_named_idx = Range.tl c.env_named_idx;
+    env_named_secvars = secvars;
+  }
+  in
+  Some (status, decl, cval)
 
 let map_named_val f ctxt =
   let open Context.Named.Declaration in
-  let fold accu d =
-    let d' = f d in
-    let accu =
-      if d == d' then accu
-      else Id.Map.set (get_id d) d' accu
+  let fold (map,secvars) d =
+    let id = get_id d in
+    let status = var_status_ctxt ~check:false id ctxt in
+    let status', d' = f status d in
+    let () = assert (Id.equal id (get_id d')) in
+    let map =
+      if d == d' then map
+      else Id.Map.set id d' map
     in
-    (accu, d')
+    let secvars =
+      if status == status' then secvars else
+        match status' with
+        | SecVar -> Id.Set.add id secvars
+        | ProofVar -> Id.Set.remove id secvars
+    in
+    ((map,secvars), d')
   in
-  let map, ctx = List.Smart.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
-  if map == ctxt.env_named_map then ctxt
+  let (map,secvars), ctx = List.Smart.fold_left_map fold (ctxt.env_named_map,ctxt.env_named_secvars) ctxt.env_named_ctx in
+  if map == ctxt.env_named_map && secvars == ctxt.env_named_secvars then ctxt
   else
     let idx = List.fold_right Range.cons ctx Range.empty in
-    { env_named_ctx = ctx; env_named_map = map; env_named_idx = idx }
+    { env_named_ctx = ctx; env_named_map = map; env_named_idx = idx; env_named_secvars = secvars }
+
+let push_named status d env =
+  {env with env_named_context = push_named_context_val status d env.env_named_context}
 
-let push_named d env =
-  {env with env_named_context = push_named_context_val d env.env_named_context}
+let mem_named_ctxt id ctxt =
+  Id.Map.mem id ctxt.env_named_map
 
-let mem_named id env =
-  Id.Map.mem id env.env_named_context.env_named_map
+let mem_named id env = mem_named_ctxt id  env.env_named_context
 
 let lookup_named id env =
   Id.Map.find id env.env_named_context.env_named_map
@@ -430,14 +474,18 @@ let fold_rel_context f env ~init =
 
 let named_context_of_val c = c.env_named_ctx
 
+let named_context_of_val_with_status c =
+  List.map (fun d -> var_status_ctxt ~check:false (NamedDecl.get_id d) c, d) c.env_named_ctx
+
 let ids_of_named_context_val c = Id.Map.domain c.env_named_map
 
 let empty_named_context = Context.Named.empty
 
-let push_named_context = List.fold_right push_named
+let push_named_context = List.fold_right (fun (status,d) env -> push_named status d env)
 
 let val_of_named_context ctxt =
-  List.fold_right push_named_context_val ctxt empty_named_context_val
+  List.fold_right (fun (status,d) ctxt -> push_named_context_val status d ctxt)
+    ctxt empty_named_context_val
 
 
 let eq_named_context_val c1 c2 =
@@ -478,15 +526,18 @@ let pop_rel_context n env =
     env_rel_context = skip n ctxt;
     env_nb_rel = env.env_nb_rel - n }
 
-let fold_named_context f env ~init =
-  let rec fold_right env =
-    match match_named_context_val env.env_named_context with
+let fold_named_context_val f sign ~init =
+  let rec fold_right sign =
+    match match_named_context_val sign with
     | None -> init
-    | Some (d, rem) ->
-        let env =
-          reset_with_named_context rem env in
-        f env d (fold_right env)
-  in fold_right env
+    | Some (status, d, rem) ->
+      f rem status d (fold_right rem)
+  in fold_right sign
+
+let fold_named_context f env ~init =
+  fold_named_context_val (fun sign status d acc ->
+      f (reset_with_named_context sign env) status d acc)
+    (named_context_val env) ~init
 
 let fold_named_context_reverse f ~init env =
   Context.Named.fold_inside f ~init:init (named_context env)
@@ -1017,12 +1068,13 @@ let apply_to_hyp ctxt id f =
   let open Context.Named.Declaration in
   let rec aux rtail ctxt =
     match match_named_context_val ctxt with
-    | Some (d, ctxt) ->
-        if Id.equal (get_id d) id then
-          push_named_context_val (f ctxt.env_named_ctx d rtail) ctxt
-        else
-          let ctxt' = aux (d::rtail) ctxt in
-          push_named_context_val d ctxt'
+    | Some (status, d, ctxt) ->
+      if Id.equal (get_id d) id then
+        let status, d' = f ctxt.env_named_ctx status d rtail in
+        push_named_context_val status d' ctxt
+      else
+        let ctxt' = aux (d::rtail) ctxt in
+        push_named_context_val status d ctxt'
     | None -> raise Hyp_not_found
   in aux [] ctxt
 
@@ -1032,7 +1084,7 @@ let remove_hyps ids check_context ctxt =
     if Id.Set.is_empty ids then ctxt, false
     else match match_named_context_val ctxt with
     | None -> empty_named_context_val, false
-    | Some (d, rctxt) ->
+    | Some (status, d, rctxt) ->
       let id0 = Context.Named.Declaration.get_id d in
       let removed = Id.Set.mem id0 ids in
       let ids = if removed then Id.Set.remove id0 ids else ids in
@@ -1041,10 +1093,10 @@ let remove_hyps ids check_context ctxt =
       else if not seen then ctxt, false
       else
         let rctxt' = ans in
-        let d' = check_context d in
-        if d == d' && rctxt == rctxt' then
+        let status', d' = check_context status d in
+        if status == status' && d == d' && rctxt == rctxt' then
           ctxt, true
-        else push_named_context_val d' rctxt', true
+        else push_named_context_val status' d' rctxt', true
   in
   fst (remove_hyps ids ctxt)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 58c43725e226..3eff5eabcb78 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -43,6 +43,7 @@ type named_context_val = private {
   (** Identifier-indexed version of [env_named_ctx] *)
   env_named_idx : Constr.named_declaration Range.t;
   (** Same as env_named_ctx but with a fast-access list. *)
+  env_named_secvars : Id.Set.t;
 }
 
 type rel_context_val = private {
@@ -110,24 +111,34 @@ val fold_rel_context :
 
 (** {5 Context of variables (section variables and goal assumptions) } *)
 
+type var_status = SecVar | ProofVar
+
+val var_status_eq : var_status -> var_status -> bool
+
+val var_status_ctxt : ?check:bool -> Id.t -> named_context_val -> var_status
+val var_status : ?check:bool -> Id.t -> env -> var_status
+
 val named_context_of_val : named_context_val -> Constr.named_context
-val val_of_named_context : Constr.named_context -> named_context_val
+val val_of_named_context : (var_status * Constr.named_declaration) list -> named_context_val
 val empty_named_context_val : named_context_val
 val ids_of_named_context_val : named_context_val -> Id.Set.t
+val named_context_of_val_with_status : named_context_val -> (var_status * named_declaration) list
 
 
 (** [map_named_val f ctxt] apply [f] to the body and the type of
    each declarations.
-   *** /!\ ***   [f t] should be convertible with t, and preserve the name *)
+   *** /!\ ***   [f t] must preserve the name *)
 val map_named_val :
-   (named_declaration -> named_declaration) -> named_context_val -> named_context_val
+  (var_status -> named_declaration -> var_status * named_declaration) ->
+  named_context_val -> named_context_val
 
-val push_named : Constr.named_declaration -> env -> env
-val push_named_context : Constr.named_context -> env -> env
+val push_named : var_status -> Constr.named_declaration -> env -> env
+val push_named_context : (var_status * Constr.named_declaration) list -> env -> env
 val push_named_context_val  :
-    Constr.named_declaration -> named_context_val -> named_context_val
+  var_status -> Constr.named_declaration -> named_context_val -> named_context_val
 
 
+val mem_named_ctxt : variable -> named_context_val -> bool
 val mem_named : variable -> env -> bool
 
 (** Looks up in the context of local vars referred by names ([named_context])
@@ -141,10 +152,15 @@ val named_body : variable -> env -> constr option
 
 (** {6 Recurrence on [named_context]: older declarations processed first } *)
 
+val fold_named_context_val :
+  (named_context_val -> var_status -> Constr.named_declaration -> 'a -> 'a) ->
+  named_context_val -> init:'a -> 'a
+
 val fold_named_context :
-  (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> var_status -> Constr.named_declaration -> 'a -> 'a) ->
+  env -> init:'a -> 'a
 
-val match_named_context_val : named_context_val -> (named_declaration * named_context_val) option
+val match_named_context_val : named_context_val -> (var_status * named_declaration * named_context_val) option
 
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
@@ -470,10 +486,10 @@ exception Hyp_not_found
    return [tail::(f head (id,_,_) (rev tail))::head].
    the value associated to id should not change *)
 val apply_to_hyp : named_context_val -> variable ->
-  (Constr.named_context -> Constr.named_declaration -> Constr.named_context -> Constr.named_declaration) ->
+  (Constr.named_context -> var_status -> Constr.named_declaration -> Constr.named_context -> var_status * Constr.named_declaration) ->
     named_context_val
 
-val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> named_context_val -> named_context_val
+val remove_hyps : Id.Set.t -> (var_status -> Constr.named_declaration -> var_status * Constr.named_declaration) -> named_context_val -> named_context_val
 
 val is_polymorphic : env -> Names.GlobRef.t -> bool
 val is_template_polymorphic : env -> GlobRef.t -> bool
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c91523b7cc6a..4e285f1d5d25 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -735,7 +735,7 @@ let safe_push_named d env =
       let _ = Environ.lookup_named id env in
       CErrors.user_err Pp.(pr_sequence str ["Identifier"; Id.to_string id; "already defined."])
     with Not_found -> () in
-  Environ.push_named d env
+  Environ.push_named SecVar d env
 
 let push_named_def (id,de) senv =
   let sections = get_section senv.sections in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index cef4fa076b0c..7657a7741223 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -170,34 +170,16 @@ let type_of_variable env id =
 (* Management of context of variables. *)
 
 (* Checks if a context of variables can be instantiated by the
-   variables of the current env.
-   Order does not have to be checked assuming that all names are distinct *)
-let check_hyps_inclusion env ?evars c sign =
-  let conv env a b = conv env ?evars a b in
-  Context.Named.fold_outside
-    (fun d1 () ->
-      let open Context.Named.Declaration in
-      let id = NamedDecl.get_id d1 in
-      try
-        let d2 = lookup_named id env in
-        let () = match conv env (get_type d2) (get_type d1) with
-        | Result.Ok () -> ()
-        | Result.Error () -> raise NotConvertible
-        in
-        (match d2,d1 with
-        | LocalAssum _, LocalAssum _ -> ()
-        | LocalAssum _, LocalDef _ ->
-            (* This is wrong, because we don't know if the body is
-               needed or not for typechecking: *) ()
-        | LocalDef _, LocalAssum _ -> raise NotConvertible
-        | LocalDef (_,b2,_), LocalDef (_,b1,_) ->
-          match conv env b2 b1 with
-          | Result.Ok () -> ()
-          | Result.Error () -> raise NotConvertible);
-      with Not_found | NotConvertible | Option.Heterogeneous ->
-        error_reference_variables env id c)
-    sign
-    ~init:()
+   variables of the current env. *)
+let check_hyps_inclusion env c sign =
+  sign |> List.iter @@ fun d ->
+  let id = NamedDecl.get_id d in
+  let ok =
+    match var_status ~check:false id env with
+    | SecVar -> true
+    | ProofVar -> false
+  in
+  if not ok then error_reference_variables env id c
 
 (* Instantiation of terms on real arguments. *)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d9a47916cc16..c0d94ec8d555 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -72,8 +72,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * UVars.AbstractContex
 (** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> ?evars:CClosure.evar_handler ->
-  GlobRef.t -> Constr.named_context -> unit
+val check_hyps_inclusion : env -> GlobRef.t -> Constr.named_context -> unit
 
 (** Types for primitives *)
 
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 3724149b3c1f..37187f2f930f 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -895,7 +895,7 @@ let new_state_var typ state =
   let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in
   let id = Namegen.next_ident_away __eps__ ids in
   let r = EConstr.ERelevance.relevant in (* TODO relevance *)
-  state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot id r,typ)) state.env;
+  state.env<- EConstr.push_named ProofVar (Context.Named.Declaration.LocalAssum (make_annot id r,typ)) state.env;
   id
 
 let complete_one_class state i=
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 68e9d6e99aeb..a56278ad75dd 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -31,10 +31,10 @@ let rec fill_assumptions env sigma = function
         ~typeclass_candidate:false t
     in
     let decl = LocalDef (na,ev,t) in
-    let sigma, env, ctx = fill_assumptions (EConstr.push_named decl env) sigma ctx in
+    let sigma, env, ctx = fill_assumptions (EConstr.push_named ProofVar decl env) sigma ctx in
     sigma, env, decl :: ctx
   | LocalDef _ as decl :: ctx ->
-    let sigma, env, ctx = fill_assumptions (EConstr.push_named decl env) sigma ctx in
+    let sigma, env, ctx = fill_assumptions (EConstr.push_named ProofVar decl env) sigma ctx in
     sigma, env, decl :: ctx
 
 (** [start_deriving f suchthat lemma] starts a proof of [suchthat]
@@ -70,7 +70,7 @@ let start_deriving ~atts bl suchthat name : Declare.Proof.t =
       | LocalDef (id, c, t) as d :: ctx ->
         TCons ( env , sigma , t , (fun sigma ef' ->
             let sigma = Evd.define (fst (EConstr.destEvar sigma ef')) c sigma in
-            aux (EConstr.push_named d env) sigma ctx)) in
+            aux (EConstr.push_named ProofVar d env) sigma ctx)) in
     aux env sigma ctx' in
   let kind = Decls.(IsDefinition Definition) in
   let info = Declare.Info.make ~poly ~kind () in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 4d9dac9c8fac..697be94d02a8 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -748,11 +748,7 @@ let rec extract_term table env sg mle mlt c args =
     | Evar _ | Meta _ -> MLaxiom "evar"
     | Var v ->
        (* Only during Show Extraction *)
-       let open Context.Named.Declaration in
-       let ty = match EConstr.lookup_named v env with
-         | LocalAssum (_,ty) -> ty
-         | LocalDef (_,_,ty) -> ty
-       in
+       let ty = Context.Named.Declaration.get_type @@ EConstr.lookup_named v env in
        let vty = extract_type table env sg [] 0 ty [] in
        let r = { glob = GlobRef.VarRef v; inst = InfvInst.empty } in
        let extract_var mlt = put_magic (mlt,vty) (MLglob r) in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 96dc5ee2aa4a..7238bc3eb7c3 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -800,7 +800,7 @@ let generalize_non_dep hyp =
               Id.List.mem hyp hyps
               || List.exists (Termops.occur_var_in_decl env sigma hyp) keep
               || Termops.occur_var env sigma hyp hyp_typ
-              || Termops.is_section_variable (Global.env ()) hyp
+              || Termops.is_section_variable_env env hyp
               (* should be dangerous *)
             then (clear, decl :: keep)
             else (hyp :: clear, keep))
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8cc89c153d3c..138548108a0d 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -73,7 +73,7 @@ let compute_new_princ_type_from_rel env rel_to_fun sorts princ_type =
     List.map_i change_predicate_sort 0 princ_type_info.predicates
   in
   let env_with_params_and_predicates =
-    List.fold_right Environ.push_named new_predicates env_with_params
+    List.fold_right (Environ.push_named ProofVar) new_predicates env_with_params
   in
   let rel_as_kn =
     fst
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 04a8ece16bfd..9806eea7b056 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -54,7 +54,7 @@ let build_newrecursive lnameargsardef =
         let open Context.Named.Declaration in
         let r = ERelevance.relevant in
         (* TODO relevance *)
-        ( EConstr.push_named
+        ( EConstr.push_named ProofVar
             (LocalAssum (Context.make_annot recname r, arity))
             env
         , Id.Map.add recname impl impls ))
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6793af714b96..0138c0d71c03 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -310,8 +310,8 @@ let raw_push_named (na, raw_value, raw_typ) env =
     let na = make_annot id ERelevance.relevant in
     (* TODO relevance *)
     match raw_value with
-    | None -> EConstr.push_named (NamedDecl.LocalAssum (na, typ)) env
-    | Some value -> EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env
+    | None -> EConstr.push_named ProofVar (NamedDecl.LocalAssum (na, typ)) env
+    | Some value -> EConstr.push_named ProofVar (NamedDecl.LocalDef (na, value, typ)) env
     )
 
 let add_pat_variables sigma pat typ env : Environ.env =
@@ -362,7 +362,7 @@ let add_pat_variables sigma pat typ env : Environ.env =
                ++ Printer.pr_lconstr_env env sigma new_t
                ++ fnl () );
              let open Context.Named.Declaration in
-             (Environ.push_named (LocalAssum (na, new_t)) env, mkVar id :: ctxt)
+             (Environ.push_named ProofVar (LocalAssum (na, new_t)) env, mkVar id :: ctxt)
            | LocalDef (({binder_name = Name id} as na), v, t) ->
              let na = {na with binder_name = id} in
              let new_t = substl ctxt t in
@@ -379,7 +379,7 @@ let add_pat_variables sigma pat typ env : Environ.env =
                ++ Printer.pr_lconstr_env env sigma new_v
                ++ fnl () );
              let open Context.Named.Declaration in
-             ( Environ.push_named (LocalDef (na, new_v, new_t)) env
+             ( Environ.push_named ProofVar (LocalDef (na, new_v, new_t)) env
              , mkVar id :: ctxt ))
          (Environ.rel_context new_env)
          ~init:(env, []))
@@ -643,7 +643,7 @@ let rec build_entry_lc env sigma funnames avoid rt :
       match n with
       | Anonymous -> env
       | Name id ->
-        EConstr.push_named
+        EConstr.push_named ProofVar
           (NamedDecl.LocalDef (make_annot id v_r, v_as_constr, v_type))
           env
     in
@@ -1318,7 +1318,7 @@ let do_build_inductive evd (funconstants : pconstant list)
         let u = EConstr.EInstance.make u in
         let evd, t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in
         ( evd
-        , EConstr.push_named (LocalAssum (make_annot id ERelevance.relevant, t)) env
+        , EConstr.push_named ProofVar (LocalAssum (make_annot id ERelevance.relevant, t)) env
         ))
       funnames
       (Array.of_list funconstants)
@@ -1379,7 +1379,7 @@ let do_build_inductive evd (funconstants : pconstant list)
         in
         let r = ERelevance.relevant in
         (* TODO relevance *)
-        EConstr.push_named (LocalAssum (make_annot rel_name r, rex)) env)
+        EConstr.push_named ProofVar (LocalAssum (make_annot rel_name r, rex)) env)
       env relnames rel_arities
   in
   (* and of the real constructors*)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 4809a1ef05e1..623e3df74438 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -589,8 +589,7 @@ let resolve_and_replace_implicits exptyp env sigma rt =
       undeclared_evars_rr = false;
       unconstrained_sorts = false;
     } in
-    let hypnaming = Evarutil.VarSet.variables (Global.env ()) in
-    let genv = GlobEnv.make ~hypnaming env sigma Glob_ops.empty_lvar in
+    let genv = GlobEnv.make env sigma Glob_ops.empty_lvar in
     let pretyper = { default_pretyper with pretype_hole; pretype_type } in
     let sigma', _ = eval_pretyper pretyper ~flags:pretype_flags (Some exptyp) genv sigma rt in
     solve_remaining_evars flags env ~initial:sigma sigma'
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 41a8bdc4c9ec..0d81630d88e6 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1630,9 +1630,8 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
   let function_r = ERelevance.relevant in
   (* TODO relevance *)
   let env =
-    EConstr.push_named
-      (Context.Named.Declaration.LocalAssum
-         (make_annot function_name function_r, function_type))
+    EConstr.push_named ProofVar
+      (LocalAssum (make_annot function_name function_r, function_type))
       env
   in
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index fc0cb6611fe0..30c7aff4d81b 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -505,6 +505,10 @@ TACTIC EXTEND is_hyp
 | [ "is_var" constr(x) ] -> { Internals.is_var x }
 END
 
+TACTIC EXTEND is_secvar
+| [ "is_section_var" constr(x) ] -> { Internals.is_section_var x }
+END
+
 TACTIC EXTEND is_fix
 | [ "is_fix" constr(x) ] -> { Internals.is_fix x }
 END
diff --git a/plugins/ltac/internals.ml b/plugins/ltac/internals.ml
index 7bf5ab378113..53a8b4175fb1 100644
--- a/plugins/ltac/internals.ml
+++ b/plugins/ltac/internals.ml
@@ -126,6 +126,20 @@ let is_var x =
     | Var _ ->  Proofview.tclUNIT ()
     | _ -> Tacticals.tclFAIL (Pp.str "Not a variable or hypothesis")
 
+let is_section_var x =
+  (* we can enter_one because a constr argument is focusing *)
+  Proofview.Goal.enter_one ~__LOC__ begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    match EConstr.kind sigma x with
+    | Var id ->
+      (* check:false because we don't want to anomaly here if the user
+         sneaks in some unbound variable *)
+      if Termops.is_section_variable_env ~check:false env id then Proofview.tclUNIT ()
+      else Tacticals.tclFAIL (Pp.str "Not a section variable.")
+    | _ -> Tacticals.tclFAIL (Pp.str "Not a variable or hypothesis.")
+  end
+
 let is_fix x =
   Proofview.tclEVARMAP >>= fun sigma ->
   match EConstr.kind sigma x with
diff --git a/plugins/ltac/internals.mli b/plugins/ltac/internals.mli
index 027debcc3ac8..3d9090326c71 100644
--- a/plugins/ltac/internals.mli
+++ b/plugins/ltac/internals.mli
@@ -44,6 +44,7 @@ val refine_tac : Tacinterp.interp_sign -> simple:bool -> with_classes:bool ->
 val has_evar : EConstr.t -> unit tactic
 val is_evar : EConstr.t -> unit tactic
 val is_var : EConstr.t -> unit tactic
+val is_section_var : EConstr.t -> unit tactic
 val is_fix : EConstr.t -> unit tactic
 val is_cofix : EConstr.t -> unit tactic
 val is_ind : EConstr.t -> unit tactic
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 5920390ea1c1..11e896c380d6 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -118,11 +118,11 @@ let rec add_prods_sign env sigma t =
     | Prod (na,c1,b) ->
         let id = id_of_name_using_hdchar env sigma t na.binder_name in
         let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
+        add_prods_sign (push_named ProofVar (LocalAssum ({na with binder_name=id},c1)) env) sigma b'
     | LetIn (na,c1,t1,b) ->
         let id = id_of_name_using_hdchar env sigma t na.binder_name in
         let b'= subst1 (mkVar id) b in
-        add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
+        add_prods_sign (push_named ProofVar (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b'
     | _ -> (env,t)
 
 (* [dep_option] indicates whether the inversion lemma is dependent or not.
@@ -156,8 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       let ivars = Termops.global_vars_set env sigma i in
       let revargs,ownsign =
         fold_named_context
-          (fun env d (revargs,hyps) ->
-            let d = EConstr.of_named_decl d in
+          (fun env status d (revargs,hyps) ->
              let id = NamedDecl.get_id d in
              if Id.Set.mem id ivars then
                ((mkVar id)::revargs, Context.Named.add d hyps)
@@ -170,7 +169,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
       (pty,goal)
   in
   let npty = nf_all env sigma pty in
-  let extenv = push_named (LocalAssum (make_annot p ERelevance.relevant,npty)) env in
+  let extenv = push_named ProofVar (LocalAssum (make_annot p ERelevance.relevant,npty)) env in
   extenv, goal
 
 (* [inversion_scheme sign I]
@@ -201,12 +200,10 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
   let pf = Proof.start ~name ~poly (Evd.from_ustate (ustate sigma)) [invEnv,invGoal] in
   let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in
   let pfterm = List.hd (Proof.partial_proof pf) in
-  let global_named_context = Global.named_context_val () in
   let ownSign = ref begin
     fold_named_context
-      (fun env d sign ->
-        let d = EConstr.of_named_decl d in
-         if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
+      (fun env status d sign ->
+         if status = SecVar then sign
          else Context.Named.add d sign)
       invEnv ~init:Context.Named.empty
   end in
diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index a31622747735..38ca97720bc7 100644
--- a/plugins/ltac2/tac2core.ml
+++ b/plugins/ltac2/tac2core.ml
@@ -754,7 +754,7 @@ let () =
         let sigma, j = Typing.type_judgment env sigma {uj_val=t; uj_type=t_ty} in
         sigma, EConstr.ESorts.relevance_of_sort j.utj_type
       in
-      let nenv = EConstr.push_named (LocalAssum (Context.make_annot id t_rel, t)) env in
+      let nenv = EConstr.push_named ProofVar (LocalAssum (Context.make_annot id t_rel, t)) env in
       let (sigma, (evt, s)) = Evarutil.new_type_evar nenv sigma Evd.univ_flexible in
       let relevance = EConstr.ESorts.relevance_of_sort s in
       let (sigma, evk) = Evarutil.new_pure_evar (Environ.named_context_val nenv) sigma ~relevance evt in
diff --git a/plugins/ltac2/tac2tactics.ml b/plugins/ltac2/tac2tactics.ml
index 29e79d142628..5efd07b530bc 100644
--- a/plugins/ltac2/tac2tactics.ml
+++ b/plugins/ltac2/tac2tactics.ml
@@ -447,7 +447,7 @@ let wrap_tactic_call f =
   let open Proofview.Notations in
   let wrapf ~env ~carrier ~lhs ~rel =
     Proofview.tclEVARMAP >>= fun sigma ->
-      let ectx = ext_named_context_of_env ~hypnaming:Evarutil.VarSet.empty env sigma in
+      let ectx = ext_named_context_of_env env sigma in
       let subst = ext_csubst ectx in
       let carriern = Evarutil.csubst_subst sigma subst carrier in
       let lhsn = Evarutil.csubst_subst sigma subst lhs in
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 823b345fe104..7d4cdc2f20a6 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -1335,7 +1335,7 @@ let trans_check_prop env evd t =
 
 let get_hyp_typ = function
   | NamedDecl.LocalDef (h, _, ty) | NamedDecl.LocalAssum (h, ty) ->
-    (h.Context.binder_name, EConstr.of_constr ty)
+    (h.Context.binder_name, ty)
 
 let trans_hyps env evd l =
   List.fold_left
@@ -1449,7 +1449,7 @@ let zify_tac =
       init_cache ();
       let evd = Proofview.Goal.sigma gl in
       let env = Proofview.Goal.env gl in
-      let sign = Environ.named_context env in
+      let sign = EConstr.named_context env in
       let concl = Proofview.Goal.concl gl in
       let evd, concl = trans_check_prop env evd concl in
       let evd, hyps = trans_hyps env evd sign in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 4d2a659b2702..e79cb3d6be9c 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -47,7 +47,7 @@ let hyp_id (SsrHyp (_, id)) = id
 let hyp_err ?loc msg id =
   CErrors.user_err ?loc Pp.(str msg ++ Id.print id)
 
-let not_section_id id = not (Termops.is_section_variable (Global.env ()) id)
+let not_section_id id = not (Termops.is_section_variable (Global.env ()) id) [@@warning "-3"]
 
 let hyps_ids = List.map hyp_id
 
@@ -1203,7 +1203,7 @@ let unsafe_intro env decl ~relevance b =
   let open Context.Named.Declaration in
   Refine.refine_with_principal ~typecheck:false begin fun sigma ->
     let ctx = Environ.named_context_val env in
-    let nctx = EConstr.push_named_context_val decl ctx in
+    let nctx = EConstr.push_named_context_val ProofVar decl ctx in
     let inst = EConstr.identity_subst_val (Environ.named_context_val env) in
     let ninst = SList.cons (EConstr.mkRel 1) inst in
     let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
@@ -1212,8 +1212,10 @@ let unsafe_intro env decl ~relevance b =
   end
 
 let set_decl_id id = let open Context in function
-  | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum({name with binder_name=id},ty)
-  | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef({name with binder_name=id},ty,t)
+  | Rel.Declaration.LocalAssum(name,ty) ->
+    Named.Declaration.LocalAssum({name with binder_name=id},ty)
+  | Rel.Declaration.LocalDef(name,ty,t) ->
+    Named.Declaration.LocalDef({name with binder_name=id},ty,t)
 
 let rec decompose_assum env sigma orig_goal =
   let open Context in
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 20a04f31661a..1a2aaa97c846 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -291,7 +291,7 @@ let intro_clear ids =
     let env = Proofview.Goal.env gl in
     let fold (used_ids, clear_ids, ren) id =
       let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in
-      let used_ids = Environ.push_named_context_val (LocalAssum (annotR new_id, mkProp)) used_ids in
+      let used_ids = Environ.push_named_context_val ProofVar (LocalAssum (annotR new_id, mkProp)) used_ids in
       (used_ids, new_id :: clear_ids, (id, new_id) :: ren)
     in
     let _, clear_ids, ren = List.fold_left fold (Environ.named_context_val env, [], []) ids in
@@ -748,9 +748,9 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
       if not (EConstr.isVar sigma c) then
         Ssrcommon.errorstrm Pp.(str "@ can be used with variables only")
       else match Context.Named.lookup (EConstr.destVar sigma c) hyps with
-      | Context.Named.Declaration.LocalAssum _ ->
+      | LocalAssum _ ->
           Ssrcommon.errorstrm Pp.(str "@ can be used with let-ins only")
-      | Context.Named.Declaration.LocalDef (name, b, ty) ->
+      | LocalDef (name, b, ty) ->
           Unsafe.tclEVARS sigma <*>
           tclUNIT (true, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl), c, clr)
     else
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index bd858fc96026..866e2d65d057 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -447,7 +447,7 @@ let pr_econstr_pat env sigma c0 =
     let dummy_prod = mkProd (make_annot Anonymous Sorts.Relevant,mkProp,mkProp) in
     let na = make_annot (EConstr.destVar sigma ehole_var) Sorts.Relevant in
     Context.Named.Declaration.(LocalAssum (na, dummy_prod)) in
-  let env = Environ.push_named dummy_decl env in
+  let env = Environ.push_named ProofVar dummy_decl env in
   pr_econstr_env env sigma (wipe_evar c0)
 
 (* Turn (new) evars into metas *)
@@ -1166,6 +1166,8 @@ let thin id sigma goal =
   let cl = Evd.evar_concl evi in
   let relevance = Evd.evar_relevance evi in
   let ans =
+    (* Why can this get called with an unknown id? *)
+    if not @@ Environ.mem_named id env then Some (sigma, Environ.named_context_val env, cl) else
     try Some (Evarutil.clear_hyps_in_evi env sigma (Environ.named_context_val env) cl ids)
     with Evarutil.ClearDependencyError _ -> None
   in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 36f2de210cb7..cf314eaa01f5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -504,11 +504,10 @@ let remove_current_pattern eqn =
     | [] -> anomaly (Pp.str "Empty list of patterns.")
 
 let push_current_pattern ~program_mode sigma (cur,ty) eqn =
-  let hypnaming = VarSet.variables (Global.env ()) in
   match eqn.patterns with
     | pat::pats ->
         let r = ERelevance.relevant in (* TODO relevance *)
-        let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (make_annot (alias_of_pat pat) r,cur,ty)) eqn.rhs.rhs_env in
+        let _,rhs_env = push_rel sigma (LocalDef (make_annot (alias_of_pat pat) r,cur,ty)) eqn.rhs.rhs_env in
         { eqn with
             rhs = { eqn.rhs with rhs_env = rhs_env };
             patterns = pats }
@@ -860,9 +859,9 @@ let recover_and_adjust_alias_names (_,avoid) names sign =
   in
   List.split (aux (names,sign))
 
-let push_rels_eqn ~hypnaming sigma sign eqn =
+let push_rels_eqn sigma sign eqn =
   {eqn with
-     rhs = {eqn.rhs with rhs_env = snd (push_rel_context ~hypnaming sigma sign eqn.rhs.rhs_env) } }
+     rhs = {eqn.rhs with rhs_env = snd (push_rel_context sigma sign eqn.rhs.rhs_env) } }
 
 let push_rels_eqn_with_names sigma sign eqn =
   let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in
@@ -870,12 +869,12 @@ let push_rels_eqn_with_names sigma sign eqn =
   let sign = recover_initial_subpattern_names subpatnames sign in
   push_rels_eqn sigma sign eqn
 
-let push_generalized_decl_eqn ~hypnaming env sigma n decl eqn =
+let push_generalized_decl_eqn env sigma n decl eqn =
   match RelDecl.get_name decl with
   | Anonymous ->
-      push_rels_eqn ~hypnaming sigma [decl] eqn
+      push_rels_eqn sigma [decl] eqn
   | Name _ ->
-      push_rels_eqn ~hypnaming sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
+      push_rels_eqn sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
 
 let drop_alias_eqn eqn =
   { eqn with alias_stack = List.tl eqn.alias_stack }
@@ -1356,8 +1355,7 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname)
   let typs' =
     List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in
 
-  let hypnaming = VarSet.variables (Global.env ()) in
-  let typs,extenv = push_rel_context ~hypnaming sigma typs pb.env in
+  let typs,extenv = push_rel_context sigma typs pb.env in
 
   let typs' =
     List.map (fun (c,d) ->
@@ -1436,7 +1434,7 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname)
       tomatch = tomatch;
       pred = pred;
       history = history;
-      mat = List.map (push_rels_eqn_with_names ~hypnaming sigma typs) submat }
+      mat = List.map (push_rels_eqn_with_names sigma typs) submat }
 
 (**********************************************************************
  INVARIANT:
@@ -1452,7 +1450,6 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname)
 (**********************************************************************)
 (* Main compiling descent *)
 let compile ~program_mode sigma pb =
-  let hypnaming = VarSet.variables (Global.env ()) in
   let rec compile sigma pb =
     match pb.tomatch with
       | Pushed cur :: rest -> match_current sigma { pb with tomatch = rest } cur
@@ -1519,7 +1516,7 @@ let compile ~program_mode sigma pb =
     let env = Name.fold_left (fun env id -> hide_variable env id) pb.env na in
     let pb =
       { pb with
-         env = snd (push_rel ~hypnaming sigma (LocalDef (annotR na,current,ty)) env);
+         env = snd (push_rel sigma (LocalDef (annotR na,current,ty)) env);
          tomatch = tomatch;
          pred = lift_predicate 1 pred tomatch;
          history = pop_history pb.history;
@@ -1556,9 +1553,9 @@ let compile ~program_mode sigma pb =
   and compile_generalization sigma pb i d rest =
     let pb =
       { pb with
-         env = snd (push_rel ~hypnaming sigma d pb.env);
+         env = snd (push_rel sigma d pb.env);
          tomatch = rest;
-         mat = List.map (push_generalized_decl_eqn ~hypnaming pb.env sigma i d) pb.mat } in
+         mat = List.map (push_generalized_decl_eqn pb.env sigma i d) pb.mat } in
     let used, sigma, j = compile sigma pb in
     used, sigma, { uj_val = mkLambda_or_LetIn d j.uj_val;
       uj_type = mkProd_wo_LetIn d j.uj_type }
@@ -1572,11 +1569,11 @@ let compile ~program_mode sigma pb =
       let alias = LocalDef (make_annot na r,c,t) in
       let pb =
         { pb with
-           env = snd (push_rel ~hypnaming sigma alias pb.env);
+           env = snd (push_rel sigma alias pb.env);
            tomatch = lift_tomatch_stack 1 rest;
            pred = lift_predicate 1 pb.pred pb.tomatch;
            history = pop_history_pattern pb.history;
-           mat = List.map (push_alias_eqn ~hypnaming sigma alias) pb.mat } in
+           mat = List.map (push_alias_eqn sigma alias) pb.mat } in
       let used, sigma, j = compile sigma pb in
       used, sigma, { uj_val =
           if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then
@@ -1718,8 +1715,7 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
   (subst0, t0)
 
 let push_binder sigma d (k,env,subst) =
-  let hypnaming = VarSet.variables (Global.env ()) in
-  (k+1,snd (push_rel ~hypnaming sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
+  (k+1,snd (push_rel sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
 
 let rec list_assoc_in_triple x = function
     [] -> raise Not_found
@@ -1842,7 +1838,6 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t =
  *)
 
 let build_inversion_problem ~program_mode loc env sigma tms t =
-  let hypnaming = VarSet.variables (Global.env ()) in
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd !!env sigma t Anonymous) avoid in
     DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in
@@ -1867,14 +1862,14 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
         let patl = pat :: List.rev patl in
         let patl,sign = recover_and_adjust_alias_names acc patl sign in
         let p = List.length patl in
-        let _,env' = push_rel_context ~hypnaming sigma sign env in
+        let _,env' = push_rel_context sigma sign env in
         let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
         List.rev_append patl patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
       let pat,acc = make_patvar t acc in
       let typ = lift n typ in
       let d = LocalAssum (annotR (alias_of_pat pat),typ) in
-      let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming sigma d env)) (d::acc_sign) tms acc in
+      let patl,acc_sign,acc = aux (n+1) (snd (push_rel sigma d env)) (d::acc_sign) tms acc in
       pat::patl,acc_sign,acc in
   let avoid0 = GlobEnv.vars_of_env env in
   (* [patl] is a list of patterns revealing the substructure of
@@ -1892,7 +1887,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
   let decls =
     List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in
 
-  let _,pb_env = push_rel_context ~hypnaming sigma sign env in
+  let _,pb_env = push_rel_context sigma sign env in
   let decls =
     List.map (fun (c,d) -> (c,extract_inductive_data !!(pb_env) sigma d,d)) decls in
 
@@ -2102,8 +2097,7 @@ let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs ars
   in
   assert (len == 0);
   let p = predicate 0 c in
-  let hypnaming = VarSet.variables (Global.env ()) in
-  let arsign,env' = List.fold_right_map (push_rel_context ~hypnaming sigma) arsign env in
+  let arsign,env' = List.fold_right_map (push_rel_context sigma) arsign env in
   try let sigma' = fst (Typing.type_of !!env' sigma p) in
         Some (sigma', p, arsign)
   with e when precatchable_exception e -> None
@@ -2165,8 +2159,7 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty
     (* Some type annotation *)
     | Some rtntyp ->
       (* We extract the signature of the arity *)
-      let hypnaming = VarSet.variables (Global.env ()) in
-      let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming sigma) arsign env in
+      let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
       let sigma, rtnsort = Evd.new_sort_variable univ_flexible sigma in
       let sigma, predcclj = typing_fun (Some (mkSort rtnsort)) envar sigma rtntyp in
       let check_elim_sort sigma squash =
@@ -2420,7 +2413,6 @@ let build_ineqs env sigma prevpatterns curpats curpat_sign_len =
 
 let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity =
   let i = ref 0 in
-  let hypnaming = VarSet.variables (Global.env ()) in
   let (sigma, x, y, z) =
     List.fold_left
       (fun (sigma, branches, eqns, prevpatterns) eqn ->
@@ -2483,7 +2475,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity =
            let eqs_rels, arity = decompose_prod_n_decls sigma neqs arity in
              eqs_rels @ neqs_rels @ rhs_rels', arity
          in
-         let _,rhs_env = push_rel_context ~hypnaming sigma rhs_rels' env in
+         let _,rhs_env = push_rel_context sigma rhs_rels' env in
          let sigma, j = typing_fun (mk_tycon tycon) rhs_env sigma eqn.rhs.it in
          let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
          and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
@@ -2697,7 +2689,6 @@ let context_of_arsign l =
 
 let compile_program_cases ?loc style (typing_function, sigma) tycon env
     (predopt, tomatchl, eqns) =
-  let hypnaming = VarSet.variables (Global.env ()) in
   let typing_fun tycon env sigma = function
     | Some t ->	typing_function tycon env sigma t
     | None -> coq_unit_judge !!env sigma in
@@ -2710,7 +2701,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
   let env, sigma, tomatchs = coerce_to_indtype ~program_mode:true typing_function env sigma matx tomatchl in
   let tycon = valcon_of_tycon tycon in
   let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env sigma tomatchs tycon in
-  let _,env = push_rel_context ~hypnaming sigma tomatchs_lets env in
+  let _,env = push_rel_context sigma tomatchs_lets env in
   let len = List.length eqns in
   let sigma, sign, signlen, eqs, args =
     (* The arity signature *)
@@ -2746,7 +2737,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env
   in
   let matx = List.rev matx in
   let _ = assert (Int.equal len (List.length lets)) in
-  let _,env = push_rel_context ~hypnaming sigma lets env in
+  let _,env = push_rel_context sigma lets env in
   let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
   let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
   let args = List.rev_map (lift len) args in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 5f7751267b0b..03ecfe8774b0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1818,7 +1818,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
      debug_ho_unification (fun () ->
        Pp.(str"abstracted: " ++ prc env_rhs evd rhs'));
      let () = check_selected_occs env_rhs evd c !occ occs in
-     let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in
+     let env_rhs' = push_named ProofVar (NamedDecl.LocalAssum (id,idty)) env_rhs in
      set_holes env_rhs' evd fixed rhs' subst
   | [] -> evd, fixed, rhs in
 
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 11f79dc6968e..367c02df12cc 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -86,7 +86,7 @@ let define_pure_evar_as_product env evd na evk =
   in
   let rdom = ESorts.relevance_of_sort u1 in
   let evd2,rng =
-    let newenv = push_named (LocalAssum (make_annot id rdom, dom)) evenv in
+    let newenv = push_named ProofVar (LocalAssum (make_annot id rdom, dom)) evenv in
     let src = subterm_source evk ~where:Codomain evksrc in
     let filter = Filter.extend 1 (evar_filter evi) in
       if Environ.is_impredicative_sort env (ESorts.kind evd1 s) then
@@ -139,7 +139,7 @@ let define_pure_evar_as_lambda env evd name evk =
     map_annot (fun na -> next_name_away_with_default_using_types evenv evd "x" na avoid
       (Reductionops.whd_evar evd dom)) na
   in
-  let newenv = push_named (LocalAssum (id, dom)) evenv in
+  let newenv = push_named ProofVar (LocalAssum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = subterm_source evk ~where:Body (evar_source evi) in
   let abstract_arguments = Abstraction.abstract_last (Evd.evar_abstract_arguments evi) in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 2f89f4e578c0..fc3ec8b698e1 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -568,7 +568,8 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c =
         | Some (RelAlias n) -> if n >= depth+1 then fv_rels := Int.Set.add (n-depth) !fv_rels
         | None -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
-        fv_ids := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !fv_ids
+        (* XXX should be Evarutil.vars_of_global to handle abstracted constants? *)
+        fv_ids := Id.Set.union (Environ.vars_of_global env (fst @@ EConstr.destRef sigma c)) !fv_ids
     | _ ->
         iter_with_full_binders env sigma
           (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1))
@@ -869,7 +870,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
           let evd,b = define_evar_from_virtual_equation define_fun env evd src b
             t_in_sign sign filter inst_in_env in
           evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
-      (push_named_context_val d' sign, Filter.extend 1 filter,
+      (push_named_context_val ProofVar d' sign, Filter.extend 1 filter,
        SList.cons (mkRel 1) (SList.Skip.map (lift 1) inst_in_env),
        SList.cons (mkRel 1) (SList.Skip.map (lift 1) inst_in_sign),
        push_rel d env,evd,Id.Set.add id.binder_name avoid))
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index fb2e18a34ab7..a2ab718571a4 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -38,8 +38,8 @@ type t = {
   lvar : ltac_var_map;
 }
 
-let make ~hypnaming env sigma lvar =
-  let get_extra env sigma = ext_named_context_of_env ~hypnaming env sigma in
+let make env sigma lvar =
+  let get_extra env sigma = ext_named_context_of_env env sigma in
   {
     static_env = env;
     renamed_env = env;
@@ -65,33 +65,33 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id =
 
 let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
 
-let push_rel ~hypnaming sigma d env =
+let push_rel sigma d env =
   let open Context.Rel.Declaration in
   let d' = map_name (ltac_interp_name env.lvar) d in
   let env = {
     static_env = push_rel d env.static_env;
     renamed_env = push_rel d' env.renamed_env;
-    extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
+    extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
   d', env
 
-let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
+let push_rel_context ?(force_names=false) sigma ctx env =
   let open Context.Rel.Declaration in
   let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in
   let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in
   let env = {
     static_env = push_rel_context ctx env.static_env;
     renamed_env = push_rel_context ctx' env.renamed_env;
-    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
+    extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra));
     lvar = env.lvar;
     } in
   ctx', env
 
-let push_rec_types ~hypnaming sigma (lna,typarray) env =
+let push_rec_types sigma (lna,typarray) env =
   let open Context.Rel.Declaration in
   let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
-  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e ~hypnaming in (e,d)) env ctxt in
+  let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in
   Array.map get_annot ctx, env
 
 let new_evar env sigma ?src ?rrpat ?(naming = Namegen.IntroAnonymous) ?relevance typ =
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 2f2f4998171f..44065277f8c8 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -13,7 +13,6 @@ open Environ
 open Evd
 open EConstr
 open Ltac_pretype
-open Evarutil
 
 (** Type of environment extended with naming and ltac interpretation data *)
 
@@ -41,7 +40,7 @@ val register_constr_interp0 :
 
 (** Build a pretyping environment from an ltac environment *)
 
-val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t
+val make : env -> evar_map -> ltac_var_map -> t
 
 (** Export the underlying environment *)
 
@@ -53,9 +52,9 @@ val vars_of_env : t -> Id.Set.t
 
 (** Push to the environment, returning the declaration(s) with interpreted names *)
 
-val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t
-val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
-val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t EConstr.binder_annot array * constr array -> t -> Name.t EConstr.binder_annot array * t
+val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t
+val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
+val push_rec_types : evar_map -> Name.t EConstr.binder_annot array * constr array -> t -> Name.t EConstr.binder_annot array * t
 
 (** Declare an evar using renaming information *)
 
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 39b51b68958c..e5d7397cf866 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -39,7 +39,7 @@ let rec compute_head_const env sigma cst =
 
 and compute_head_var env sigma id = match lookup_named id env with
 | LocalDef (_,c,_) -> kind_of_head env sigma c
-| _ -> RigidHead RigidOther
+| LocalAssum _ -> RigidHead RigidOther
 
 and kind_of_head env sigma t =
   let rec aux k l t b = match EConstr.kind sigma (Reductionops.clos_whd_flags RedFlags.betaiotazeta env sigma t) with
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1d8452d3b9d6..0fed7ee86bd1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -31,7 +31,7 @@ let type_of_inductive env (ind,u) =
 
 let e_type_of_inductive env sigma (ind,u) =
  let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
- Reductionops.check_hyps_inclusion env sigma (GlobRef.IndRef ind) mib.mind_hyps;
+ Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps;
  let t = Inductive.type_of_inductive (specif, EConstr.Unsafe.to_instance u) in
  EConstr.of_constr (Arguments_renaming.rename_type env t (IndRef ind))
 
@@ -47,7 +47,7 @@ let type_of_constructor env (cstr,u) =
 let e_type_of_constructor env sigma (cstr,u) =
  let (mib,_ as specif) =
    Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
- Reductionops.check_hyps_inclusion env sigma (GlobRef.ConstructRef cstr) mib.mind_hyps;
+ Typeops.check_hyps_inclusion env (GlobRef.ConstructRef cstr) mib.mind_hyps;
  let t = Inductive.type_of_constructor (cstr,EConstr.Unsafe.to_instance u) specif in
  EConstr.of_constr (Arguments_renaming.rename_type env t (ConstructRef cstr))
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2faea419716a..648d6e9c6990 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -795,27 +795,26 @@ struct
     let open Context.Rel.Declaration in
     let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in
     let pretype_type tycon env sigma c = eval_type_pretyper self ~flags tycon env sigma c in
-    let hypnaming = VarSet.variables (Global.env ()) in
     let rec type_bl env sigma ctxt = function
       | [] -> sigma, ctxt
       | (na,_,bk,None,ty)::bl ->
         let sigma, ty' = pretype_type empty_valcon env sigma ty in
         let rty' = ESorts.relevance_of_sort ty'.utj_type in
         let dcl = LocalAssum (make_annot na rty', ty'.utj_val) in
-        let dcl', env = push_rel ~hypnaming sigma dcl env in
+        let dcl', env = push_rel sigma dcl env in
         type_bl env sigma (Context.Rel.add dcl' ctxt) bl
       | (na,_,bk,Some bd,ty)::bl ->
         let sigma, ty' = pretype_type empty_valcon env sigma ty in
         let rty' = ESorts.relevance_of_sort ty'.utj_type in
         let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in
         let dcl = LocalDef (make_annot na rty', bd'.uj_val, ty'.utj_val) in
-        let dcl', env = push_rel ~hypnaming sigma dcl env in
+        let dcl', env = push_rel sigma dcl env in
         type_bl env sigma (Context.Rel.add dcl' ctxt) bl in
     let sigma, ctxtv = Array.fold_left_map (fun sigma -> type_bl env sigma Context.Rel.empty) sigma bl in
     let sigma, larj =
       Array.fold_left2_map
         (fun sigma e ar ->
-          pretype_type empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar)
+          pretype_type empty_valcon (snd (push_rel_context sigma e env)) sigma ar)
         sigma ctxtv lar in
     let lara = Array.map (fun a -> a.utj_val) larj in
     let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -839,7 +838,7 @@ struct
         names ftys
     in
       (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-    let names,newenv = push_rec_types ~hypnaming sigma (names,ftys) env in
+    let names,newenv = push_rec_types sigma (names,ftys) env in
     let sigma, vdefj =
       Array.fold_left2_map_i
         (fun i sigma ctxt def ->
@@ -848,7 +847,7 @@ struct
            let (ctxt,ty) =
              decompose_prod_n_decls sigma (Context.Rel.length ctxt)
                (lift nbfix ftys.(i)) in
-           let ctxt,nenv = push_rel_context ~hypnaming sigma ctxt newenv in
+           let ctxt,nenv = push_rel_context sigma ctxt newenv in
            let sigma, j = pretype (mk_tycon ty) nenv sigma def in
            sigma, { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
                     uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
@@ -1251,8 +1250,7 @@ struct
     let sigma, j = eval_type_pretyper self ~flags dom_valcon env sigma c1 in
     let name = {binder_name=name; binder_relevance=ESorts.relevance_of_sort j.utj_type} in
     let var = LocalAssum (name, j.utj_val) in
-    let hypnaming = VarSet.variables (Global.env ()) in
-    let var',env' = push_rel ~hypnaming sigma var env in
+    let var',env' = push_rel sigma var env in
     let sigma, j' = eval_pretyper self ~flags rng env' sigma c2 in
     let name = get_name var' in
     let resj = judge_of_abstraction !!env sigma (orelse_name name name') j j' in
@@ -1263,7 +1261,6 @@ struct
     let open Context.Rel.Declaration in
     let pretype_type tycon env sigma c = eval_type_pretyper self ~flags tycon env sigma c in
     let sigma, j = pretype_type empty_valcon env sigma c1 in
-    let hypnaming = VarSet.variables (Global.env ()) in
     let sigma, name, j' = match name with
       | Anonymous ->
         let sigma, j = pretype_type empty_valcon env sigma c2 in
@@ -1271,7 +1268,7 @@ struct
       | Name _ ->
         let r = ESorts.relevance_of_sort j.utj_type in
         let var = LocalAssum (make_annot name r, j.utj_val) in
-        let var, env' = push_rel ~hypnaming sigma var env in
+        let var, env' = push_rel sigma var env in
         let sigma, c2_j = pretype_type empty_valcon env' sigma c2 in
         sigma, get_name var, c2_j
     in
@@ -1302,8 +1299,7 @@ struct
     let r = Retyping.relevance_of_term !!env sigma j.uj_val in
     let var = LocalDef (make_annot name r, j.uj_val, t) in
     let tycon = lift_tycon 1 tycon in
-    let hypnaming = VarSet.variables (Global.env ()) in
-    let var, env = push_rel ~hypnaming sigma var env in
+    let var, env = push_rel sigma var env in
     let sigma, j' = pretype tycon env sigma c2 in
     let name = get_name var in
     sigma, { uj_val = mkLetIn (make_annot name r, j.uj_val, t, j'.uj_val) ;
@@ -1348,8 +1344,7 @@ struct
           | _ -> assert false
         in aux 1 1 (List.rev nal) cs.cs_args, true in
     let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in
-    let hypnaming = VarSet.variables (Global.env ()) in
-    let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in
+    let fsign,env_f = push_rel_context sigma fsign env in
     let obj sigma indt rci p v f =
       if not record then
         let f = it_mkLambda_or_LetIn f fsign in
@@ -1366,7 +1361,7 @@ struct
       let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *)
       let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in
       let nar = List.length arsgn in
-      let psign',env_p = push_rel_context ~hypnaming ~force_names:true sigma psign predenv in
+      let psign',env_p = push_rel_context ~force_names:true sigma psign predenv in
           (match po with
           | Some p ->
             let sigma, pj = pretype_type empty_valcon env_p sigma p in
@@ -1431,8 +1426,7 @@ struct
     let indt = build_dependent_inductive !!env indf in
     let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *)
     let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in
-    let hypnaming = VarSet.variables (Global.env ()) in
-    let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in
+    let psign,env_p = push_rel_context sigma psign predenv in
     let sigma, pred, p = match po with
       | Some p ->
         let sigma, pj = eval_type_pretyper self ~flags empty_valcon env_p sigma p in
@@ -1457,7 +1451,7 @@ struct
       let csgn =
         List.map (set_name Anonymous) cs_args
       in
-      let _,env_c = push_rel_context ~hypnaming sigma csgn env in
+      let _,env_c = push_rel_context sigma csgn env in
       let sigma, bj = pretype (mk_tycon pi) env_c sigma b in
       sigma, it_mkLambda_or_LetIn bj.uj_val cs_args in
     let sigma, b1 = f sigma cstrs.(0) b1 in
@@ -1675,8 +1669,7 @@ let ise_pretype_gen (flags : inference_flags) env sigma lvar kind c =
       | NoUseTC -> false
       | UseTC | UseTCForConv -> true
   } in
-  let hypnaming = VarSet.variables (Global.env ()) in
-  let env = GlobEnv.make ~hypnaming env sigma lvar in
+  let env = GlobEnv.make env sigma lvar in
   let sigma', c', c'_ty = match kind with
     | WithoutTypeConstraint ->
       let sigma, j = pretype ~flags:pretype_flags empty_tycon env sigma c in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 9195b1a1f216..e99e4ea1ee4d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1414,11 +1414,6 @@ let native_infer_conv ?(pb=Conversion.CUMUL) env sigma t1 t2 =
   infer_conv_gen { genconv = fun pb ~l2r sigma ts -> native_conv_generic pb sigma }
     ~catch_incon:true ~pb env sigma t1 t2
 
-let check_hyps_inclusion env sigma x hyps =
-  let env = Environ.set_universes (Evd.universes sigma) env in
-  let evars = Evd.evar_handler sigma in
-  Typeops.check_hyps_inclusion env ~evars x hyps
-
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
 (********************************************************************)
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index f003559812f0..2e3df384cd9c 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -283,9 +283,6 @@ val infer_conv_gen : genconv ->
   ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env ->
   evar_map -> constr -> constr -> evar_map option
 
-val check_hyps_inclusion : env -> evar_map -> GlobRef.t -> Constr.named_context -> unit
-(** [Typeops.check_hyps_inclusion] but handles evars in the environment. *)
-
 (** {6 Heuristic for Conversion with Evar } *)
 
 type state = constr * Stack.t
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 35cef4bd6ca0..8d27c6126dc1 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -136,7 +136,7 @@ let betazetaevar_applist sigma n c l =
 
 let type_of_constant env sigma (c,u) =
   let cb = lookup_constant env sigma c in
-  let () = check_hyps_inclusion env sigma (GlobRef.ConstRef c) cb.const_hyps in
+  let () = Typeops.check_hyps_inclusion env (GlobRef.ConstRef c) cb.const_hyps in
   let ty = CVars.subst_instance_constr (EConstr.Unsafe.to_instance u) cb.const_type in
   EConstr.of_constr (rename_type env ty (GlobRef.ConstRef c))
 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 78fbf193b775..c540c10f6da1 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -135,9 +135,10 @@ let judge_of_applied ~check env sigma funj argjv =
   let typ = hnf_prod_appvect env sigma (j_type funj) (Array.map j_val argjv) in
   sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ }
 
+(* XXX check_hyps_inclusion should now be cheap enough to always do *)
 let judge_of_applied_inductive_knowing_parameters ~check env sigma (ind, u) argjv =
   let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-  let () = if check then Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
+  let () = if check then Typeops.check_hyps_inclusion env (GR.IndRef ind) mib.mind_hyps in
   let sigma, paramstyp = fresh_template_context env sigma ind specif argjv in
   let u0 = EInstance.kind sigma u in
   let ty, csts = Inductive.type_of_inductive_knowing_parameters (specif, u0) paramstyp in
@@ -147,7 +148,7 @@ let judge_of_applied_inductive_knowing_parameters ~check env sigma (ind, u) argj
 
 let judge_of_applied_constructor_knowing_parameters ~check env sigma ((ind, _ as cstr), u) argjv =
   let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-  let () = if check then Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
+  let () = if check then Typeops.check_hyps_inclusion env (GR.IndRef ind) mib.mind_hyps in
   let sigma, paramstyp = fresh_template_context env sigma ind specif argjv in
   let u0 = EInstance.kind sigma u in
   let ty, csts = Inductive.type_of_constructor_knowing_parameters (cstr, u0) specif paramstyp in
@@ -413,7 +414,7 @@ let judge_of_letin env sigma name defj typj j =
 let type_of_constant env sigma (c,u) =
   let open Declarations in
   let cb = EConstr.lookup_constant env sigma c in
-  let () = Reductionops.check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in
+  let () = Typeops.check_hyps_inclusion env (GR.ConstRef c) cb.const_hyps in
   let u = EInstance.kind sigma u in
   let uctx = Declareops.constant_polymorphic_context cb in
   let csts = UVars.AbstractContext.instantiate u uctx in
@@ -424,7 +425,7 @@ let type_of_constant env sigma (c,u) =
 let type_of_inductive env sigma (ind,u) =
   let open Declarations in
   let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-  let () = Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
+  let () = Typeops.check_hyps_inclusion env (GR.IndRef ind) mib.mind_hyps in
   let u = EInstance.kind sigma u in
   let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in
   let sigma = Evd.add_poly_constraints ~src:UState.Internal sigma csts in
@@ -433,7 +434,7 @@ let type_of_inductive env sigma (ind,u) =
 let type_of_constructor env sigma ((ind,_ as ctor),u) =
   let open Declarations in
   let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
-  let () = Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in
+  let () = Typeops.check_hyps_inclusion env (GR.IndRef ind) mib.mind_hyps in
   let u = EInstance.kind sigma u in
   let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in
   let sigma = Evd.add_poly_constraints ~src:UState.Internal sigma csts in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0a01d343da4c..fa75b12120b5 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -2154,6 +2154,7 @@ let get_rigid_evars sigma c =
   | _ -> EConstr.fold sigma aux vars c in
   aux Id.Set.empty c
 
+(* XXX should we lose section variable status in the push newdecl cases? *)
 let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   let id =
     let t = match ty with Some t -> t | None -> get_type_of env sigma c in
@@ -2168,13 +2169,12 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
   in
   let likefirst = clause_with_generic_occurrences occs in
   let mkvarid () = EConstr.mkVar id in
-  let compute_dependency _ d (remvars,sign,depdecls) =
-    let d = EConstr.of_named_decl d in
+  let compute_dependency _ status d (remvars,sign,depdecls) =
     let hyp = NamedDecl.get_id d in
     if Id.Set.is_empty remvars then
     match occurrences_of_hyp hyp occs with
     | NoOccurrences, InHyp ->
-        (remvars,push_named_context_val d sign,depdecls)
+        (remvars,push_named_context_val status d sign,depdecls)
     | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
         let newdecl = replace_term_occ_decl_modulo env sigma occ test mkvarid d in
@@ -2183,17 +2183,17 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         then
           if check_occs && not (in_every_hyp occs)
           then raise (PretypeError (env,sigma,NoOccurrenceFound (c,Some hyp)))
-          else (remvars,push_named_context_val d sign, depdecls)
+          else (remvars,push_named_context_val status d sign, depdecls)
         else
-          (remvars,push_named_context_val newdecl sign, newdecl :: depdecls)
+          (remvars,push_named_context_val status newdecl sign, newdecl :: depdecls)
     | occ ->
         (* There are specific occurrences, hence not like first *)
         let newdecl = replace_term_occ_decl_modulo env sigma (AtOccs occ) test mkvarid d in
-        (remvars,push_named_context_val newdecl sign, newdecl :: depdecls)
+        (remvars,push_named_context_val status newdecl sign, newdecl :: depdecls)
     else
       (* Skip declarations if all rigid variables have not been introduced *)
       let remvars = Id.Set.remove hyp remvars in
-      (remvars,push_named_context_val d sign,depdecls)
+      (remvars,push_named_context_val status d sign,depdecls)
   in
   let vars = get_rigid_evars sigma c in
   try
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f792f9f7f252..f286f29b82af 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -855,3 +855,46 @@ let pr_lconstr_pattern_expr ~flags env sigma c : Pp.t = !term_pr.pr_lconstr_patt
 let pr_cases_pattern_expr ~flags c : Pp.t = pr_patt ~flags (pr ~flags no_after ltop) no_after ltop c
 
 let pr_binders ~flags env sigma l : Pp.t = pr_undelimited_binders ~flags spc true (pr_expr ~flags env sigma no_after ltop) l
+
+module CompactedDecl = struct
+  type t =
+    | LocalAssum of (Environ.var_status option * Id.t EConstr.binder_annot) list * EConstr.types
+    | LocalDef of (Environ.var_status option * Id.t EConstr.binder_annot) list * EConstr.constr * EConstr.types
+
+  let of_named_decl status = function
+    | Context.Named.Declaration.LocalAssum (id,t) ->
+      LocalAssum ([status,id], t)
+    | Context.Named.Declaration.LocalDef (id,v,t) ->
+      LocalDef ([status,id], v, t)
+
+  let to_tuple = function
+    | LocalAssum (ids, t) -> List.map snd ids, None, t
+    | LocalDef (ids, b, t) -> List.map snd ids, Some b, t
+end
+
+let compact_named_context sigma sign =
+  let module NamedDecl = Context.Named.Declaration in
+  let compact l status decl =
+    match decl, l with
+    | NamedDecl.LocalAssum (i,t), [] ->
+      [CompactedDecl.LocalAssum ([Some status,i],t)]
+    | NamedDecl.LocalDef (i,c,t), [] ->
+      [CompactedDecl.LocalDef ([Some status,i],c,t)]
+    | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q ->
+      if EConstr.eq_constr sigma t1 t2
+      then CompactedDecl.LocalAssum ((Some status, i1)::li, t2) :: q
+      else CompactedDecl.LocalAssum ([Some status, i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q
+    | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q ->
+      if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2
+      then CompactedDecl.LocalDef ((Some status, i1)::li, c2, t2) :: q
+      else CompactedDecl.LocalDef ([Some status, i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q
+    | NamedDecl.LocalAssum (i,t), q ->
+      CompactedDecl.LocalAssum ([Some status,i],t) :: q
+    | NamedDecl.LocalDef (i,c,t), q ->
+      CompactedDecl.LocalDef ([Some status,i],c,t) :: q
+  in
+  let ctx = EConstr.fold_named_context_val (fun _ status d acc -> compact acc status d) sign ~init:[] in
+  List.map (function
+      | CompactedDecl.LocalAssum (ids, t) -> CompactedDecl.LocalAssum (List.rev ids, t)
+      | CompactedDecl.LocalDef (ids, a, b) -> CompactedDecl.LocalDef (List.rev ids, a, b))
+    ctx
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index c1921f57fa3f..7735b7ff1856 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -96,3 +96,18 @@ val modular_constr_pr :
   flags:flags ->
   ((unit->Pp.t) -> int option -> entry_relative_level -> constr_expr -> Pp.t) ->
   (unit->Pp.t) -> int option -> entry_relative_level -> constr_expr -> Pp.t
+
+module CompactedDecl : sig
+  type t =
+    | LocalAssum of (Environ.var_status option * Id.t EConstr.binder_annot) list * EConstr.types
+    | LocalDef of (Environ.var_status option * Id.t EConstr.binder_annot) list * EConstr.constr * EConstr.types
+
+  val of_named_decl : Environ.var_status option -> EConstr.named_declaration -> t
+
+  val to_tuple : t ->
+    Id.t EConstr.binder_annot list *
+    EConstr.constr option *
+    EConstr.types
+end
+
+val compact_named_context : Evd.evar_map -> Environ.named_context_val -> CompactedDecl.t list
diff --git a/printing/printer.ml b/printing/printer.ml
index e56dcc7f2a7e..1021090fa7c4 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -22,7 +22,7 @@ open Declarations
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
-module CompactedDecl = Context.Compacted.Declaration
+module CompactedDecl = Ppconstr.CompactedDecl
 
 (* This is set on by proofgeneral proof-tree mode. But may be used for
    other purposes *)
@@ -359,37 +359,42 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*)
 
 (* Flag for compact display of goals *)
 
-let get_compact_context,set_compact_context =
-  let compact_context = ref false in
-  (fun () -> !compact_context),(fun b  -> compact_context := b)
+let { Goptions.get = get_compact_context } =
+  Goptions.declare_bool_option_and_ref ~key:["Printing";"Compact";"Contexts"] ~value:false ()
 
-let pr_compacted_decl ?flags env sigma decl =
+let { Goptions.get = print_var_status } =
+  Goptions.declare_bool_option_and_ref ~key:["Printing";"Variables";"Status"] ~value:false ()
+
+let pr_ecompacted_decl ?flags env sigma decl =
   let ids, pbody, typ = match decl with
     | CompactedDecl.LocalAssum (ids, typ) ->
-       ids, None, typ
-    | CompactedDecl.LocalDef (ids,c,typ) ->
-       (* Force evaluation *)
-       let pb = pr_lconstr_env ?flags ~inctx:true env sigma c in
-       let pb = if isCast c then surround pb else pb in
-       ids, Some pb, typ in
+      ids, None, typ
+    | CompactedDecl.LocalDef (ids, c, typ) ->
+      (* Force evaluation *)
+      let pb = pr_leconstr_env ?flags ~inctx:true env sigma c in
+      let pb = if EConstr.isCast sigma c then surround pb else pb in
+      ids, Some pb, typ in
+  let pp_status status =
+    if print_var_status() then
+      match status with
+      | None -> mt()
+      | Some SecVar -> spc() ++ pr_in_comment (str "section variable")
+      | Some ProofVar -> spc() ++ pr_in_comment (str "hypothesis")
+    else mt()
+  in
   let pids =
-    hov 0 (prlist_with_sep pr_comma (fun id -> pr_id id.binder_name) ids) in
-  let pt = pr_ltype_env ?flags env sigma typ in
+    hov 0 (prlist_with_sep pr_comma (fun (status, id) -> pr_id id.binder_name ++ pp_status status) ids) in
+  let pt = pr_letype_env ?flags env sigma typ in
   match pbody with
   | None -> hov 2 (pids ++ str" :" ++ spc () ++ pt)
   | Some pbody ->
-     hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt)
-
-let pr_ecompacted_decl ?flags env sigma (decl:EConstr.compacted_declaration) =
-  let Refl = EConstr.Unsafe.eq in
-  pr_compacted_decl ?flags env sigma decl
+    hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt)
 
-let pr_named_decl ?flags env sigma decl =
-  decl |> CompactedDecl.of_named_decl |> pr_compacted_decl ?flags env sigma
+let pr_enamed_decl ?flags env sigma status decl =
+  decl |> CompactedDecl.of_named_decl status |> pr_ecompacted_decl ?flags env sigma
 
-let pr_enamed_decl ?flags env sigma (decl:EConstr.named_declaration) =
-  let Refl = EConstr.Unsafe.eq in
-  pr_named_decl ?flags env sigma decl
+let pr_named_decl ?flags env sigma status (decl:Constr.named_declaration) =
+  pr_enamed_decl ?flags env sigma status (EConstr.of_named_decl decl)
 
 let pr_rel_decl ?flags env sigma decl =
   let na = RelDecl.get_name decl in
@@ -417,19 +422,18 @@ let pr_erel_decl ?flags env sigma (decl:EConstr.rel_declaration) =
  * It's printed out from outermost to innermost, so it's readable. *)
 
 (* Prints a signature, all declarations on the same line if possible *)
+
+let pr_named_context ?flags env sigma ctx =
+  hv 0 (prlist_with_sep (fun () -> ws 2) (fun d -> pr_named_decl ?flags env sigma None d) ctx)
+
 let pr_named_context_of ?flags env sigma =
-  let make_decl_list env d pps = pr_named_decl ?flags env sigma d :: pps in
+  let make_decl_list env status d pps = pr_named_decl ?flags env sigma (Some status) d :: pps in
   let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
   hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
 let pr_var_list_decl ?flags env sigma decl =
   hov 0 (pr_ecompacted_decl ?flags env sigma decl)
 
-let pr_named_context ?flags env sigma ne_context =
-  hv 0 (Context.Named.fold_outside
-          (fun d pps -> pps ++ ws 2 ++ pr_named_decl ?flags env sigma d)
-          ne_context ~init:(mt ()))
-
 let pr_rel_context ?(flags=current_combined()) env sigma rel_context =
   let ppflags = Ppconstr.of_printing_flags flags in
   let rel_context = EConstr.of_rel_context rel_context in
@@ -441,11 +445,11 @@ let pr_rel_context_of ?flags env sigma =
 (* Prints an env (variables and de Bruijn). Separator: newline *)
 let pr_context_unlimited ?flags env sigma =
   let sign_env =
-    Context.Compacted.fold
+    List.fold_right
       (fun d pps ->
          let pidt =  pr_ecompacted_decl ?flags env sigma d in
          (pps ++ fnl () ++ pidt))
-      (Termops.compact_named_context sigma (EConstr.named_context env)) ~init:(mt ())
+      (compact_named_context sigma (Environ.named_context_val env)) (mt ())
   in
   let db_env =
     fold_rel_context
@@ -474,7 +478,7 @@ let should_compact env sigma typ =
 let rec bld_sign_env ?flags env sigma ctxt pps =
   match ctxt with
   | [] -> pps
-  | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ ->
+  | CompactedDecl.LocalAssum (_,typ)::ctxt' when should_compact env sigma typ ->
     let pps',ctxt' = bld_sign_env_id ?flags env sigma ctxt (mt ()) true in
     (* putting simple hyps in a more horizontal flavor *)
     bld_sign_env ?flags env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps')
@@ -485,7 +489,7 @@ let rec bld_sign_env ?flags env sigma ctxt pps =
 and bld_sign_env_id ?flags env sigma ctxt pps is_start =
   match ctxt with
   | [] -> pps,ctxt
- | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ ->
+ | CompactedDecl.LocalAssum(_,typ) as d :: ctxt' when should_compact env sigma typ ->
     let pidt = pr_var_list_decl ?flags env sigma d in
     let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in
     bld_sign_env_id ?flags env sigma ctxt' pps' false
@@ -495,8 +499,8 @@ and bld_sign_env_id ?flags env sigma ctxt pps is_start =
 (* compact printing an env (variables and de Bruijn). Separator: three
    spaces between simple hyps, and newline otherwise *)
 let pr_context_limit_compact ?n ?flags env sigma =
-  let ctxt = EConstr.named_context env in
-  let ctxt = Termops.compact_named_context sigma ctxt in
+  let ctxt = Environ.named_context_val env in
+  let ctxt = compact_named_context sigma ctxt in
   let lgth = List.length ctxt in
   let n_capped =
     match n with
@@ -521,9 +525,9 @@ let { Goptions.get = print_hyps_limit } =
     ~value:None
     ()
 
-let pr_context_of ?flags env sigma = match print_hyps_limit () with
-  | None -> hv 0 (pr_context_limit_compact ?flags env sigma)
-  | Some n -> hv 0 (pr_context_limit_compact ~n ?flags env sigma)
+let pr_context_of ?flags env sigma =
+  let n = print_hyps_limit () in
+  hv 0 (pr_context_limit_compact ?n ?flags env sigma)
 
 (* display goal parts (Proof mode) *)
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 2dbcf1a553d2..7413d617f289 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -183,24 +183,18 @@ val pr_notation_interpretation_env : env -> evar_map -> glob_constr -> Pp.t
 
 (** Contexts *)
 
-(** Display compact contexts of goals (simple hyps on the same line) *)
-val set_compact_context : bool -> unit
-val get_compact_context : unit -> bool
-
 val pr_context_unlimited : ?flags:PrintingFlags.t -> env -> evar_map -> Pp.t
 val pr_ne_context_of : Pp.t -> ?flags:PrintingFlags.t -> env -> evar_map -> Pp.t
 
 val pr_named_decl : ?flags:PrintingFlags.t ->
-  env -> evar_map -> Constr.named_declaration -> Pp.t
-val pr_compacted_decl : ?flags:PrintingFlags.t ->
-  env -> evar_map -> Constr.compacted_declaration -> Pp.t
+  env -> evar_map -> var_status option -> Constr.named_declaration -> Pp.t
 val pr_rel_decl : ?flags:PrintingFlags.t ->
   env -> evar_map -> Constr.rel_declaration -> Pp.t
 
 val pr_enamed_decl : ?flags:PrintingFlags.t ->
-  env -> evar_map -> EConstr.named_declaration -> Pp.t
+  env -> evar_map -> var_status option -> EConstr.named_declaration -> Pp.t
 val pr_ecompacted_decl : ?flags:PrintingFlags.t ->
-  env -> evar_map -> EConstr.compacted_declaration -> Pp.t
+  env -> evar_map -> Ppconstr.CompactedDecl.t -> Pp.t
 val pr_erel_decl : ?flags:PrintingFlags.t ->
   env -> evar_map -> EConstr.rel_declaration -> Pp.t
 
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 54f84dd6357a..12eec5366745 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -233,13 +233,6 @@ type goal = { ty: EConstr.t; env : Environ.env; sigma : Evd.evar_map; }
 
 (* XXX: Port to proofview, one day. *)
 (* open Proofview *)
-module CDC = Context.Compacted.Declaration
-
-let to_tuple : EConstr.compacted_declaration -> (Names.Id.t EConstr.binder_annot list * 'pc option * 'pc) =
-  let open CDC in function
-    | LocalAssum(idl, tm)   -> (idl, None, tm)
-    | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm)
-
 let make_goal env sigma g =
   let evi = Evd.find_undefined sigma g in
   let env = Evd.evar_filtered_env env evi in
@@ -297,7 +290,7 @@ let goal_info ~flags goal =
   let map = ref CString.Map.empty in
   let line_idents = ref [] in
   let build_hyp_info env sigma hyp =
-    let (names, body, ty) = to_tuple hyp in
+    let (names, body, ty) = Ppconstr.CompactedDecl.to_tuple hyp in
     let open Pp in
     let idents = List.map (fun x -> Names.Id.to_string x.Context.binder_name) names in
 
@@ -318,7 +311,7 @@ let goal_info ~flags goal =
   try
     let { ty=ty; env=env; sigma } = goal in
     (* compaction is usually desired [eg for better display] *)
-    let hyps = Termops.compact_named_context sigma (EConstr.named_context env) in
+    let hyps = Ppconstr.compact_named_context sigma (Environ.named_context_val env) in
     let () = List.iter (build_hyp_info env sigma) (List.rev hyps) in
     let concl_pp = pp_of_type ~flags env sigma ty in
     ( List.rev !line_idents, !map, concl_pp )
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 25dc273883f5..1f3e0e45271d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -82,28 +82,30 @@ let reorder_context env sigma sign ord =
     user_err Pp.(str "Order list has duplicates");
   let rec step ord expected ctxt_head moved_hyps ctxt_tail =
     match ord with
-      | [] -> List.fold_left (fun accu decl -> EConstr.push_named_context_val decl accu) ctxt_head ctxt_tail
-      | top::ord' when mem_q top moved_hyps ->
-          let ((d,h),mh) = find_q top moved_hyps in
-          if occur_vars_in_decl env sigma h d then
-            user_err
-              (str "Cannot move declaration " ++ Id.print top ++ spc() ++
-              str "before " ++
-              pr_sequence Id.print
-                (Id.Set.elements (Id.Set.inter h
-                  (global_vars_set_of_decl env sigma d))) ++ str ".");
-          step ord' expected ctxt_head mh (d::ctxt_tail)
-      | _ ->
-          (match EConstr.match_named_context_val ctxt_head with
-            | None -> error_no_such_hypothesis env sigma (List.hd ord)
-            | Some (d, ctxt) ->
-                let x = NamedDecl.get_id d in
-                if Id.Set.mem x expected then
-                  step ord (Id.Set.remove x expected)
-                    ctxt (push_item x d moved_hyps) ctxt_tail
-                else
-                  step ord expected
-                    ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
+    | [] ->
+      List.fold_left (fun accu (status,decl) -> EConstr.push_named_context_val status decl accu)
+        ctxt_head ctxt_tail
+    | top::ord' when mem_q top moved_hyps ->
+      let (((status,d),h),mh) = find_q top moved_hyps in
+      if occur_vars_in_decl env sigma h d then
+        user_err
+          (str "Cannot move declaration " ++ Id.print top ++ spc() ++
+           str "before " ++
+           pr_sequence Id.print
+             (Id.Set.elements (Id.Set.inter h (global_vars_set_of_decl env sigma d))) ++
+           str ".");
+      step ord' expected ctxt_head mh ((status,d)::ctxt_tail)
+    | _ ->
+      (match EConstr.match_named_context_val ctxt_head with
+       | None -> error_no_such_hypothesis env sigma (List.hd ord)
+       | Some (status, d, ctxt) ->
+         let x = NamedDecl.get_id d in
+         if Id.Set.mem x expected then
+           step ord (Id.Set.remove x expected)
+             ctxt (push_item x (status, d) moved_hyps) ctxt_tail
+         else
+           step ord expected
+             ctxt (push_val x moved_hyps) ((status,d)::ctxt_tail)) in
   step ord ords sign mt_q []
 
 let reorder_val_context env sigma sign ord =
@@ -156,10 +158,10 @@ let split_sign env sigma hfrom l =
   let () = if not (mem_id_context hfrom l) then error_no_such_hypothesis env sigma hfrom in
   let rec splitrec left sign = match EConstr.match_named_context_val sign with
   | None -> assert false
-  | Some (d, right) ->
+  | Some (status, d, right) ->
     let hyp = NamedDecl.get_id d in
-    if Id.equal hyp hfrom then (left, right, d)
-    else splitrec (d :: left) right
+    if Id.equal hyp hfrom then (left, right, (status, d))
+    else splitrec ((status, d) :: left) right
   in
   splitrec [] l
 
@@ -177,21 +179,26 @@ let () = CErrors.register_handler (function
 
 let move_hyp env sigma toleft (left,declfrom,right) hto =
   let open EConstr in
-  let push prefix sign = List.fold_right push_named_context_val prefix sign in
-  let push_rev prefix sign = List.fold_left (fun accu d -> push_named_context_val d accu) sign prefix in
+  let idfrom = NamedDecl.get_id (snd declfrom) in
+  let push prefix sign =
+    List.fold_right (fun (status,d) sign -> push_named_context_val status d sign) prefix sign
+  in
+  let push_rev prefix sign =
+    List.fold_left (fun accu (status,d) -> push_named_context_val status d accu) sign prefix
+  in
   let rec moverec_toleft ans first middle midvars = function
     | [] -> push middle @@ push first ans
-    | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
+    | (_, d) :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
       push_rev right @@ push middle @@ push first ans
-    | d :: right ->
+    | (status, d) :: right ->
         let hyp = NamedDecl.get_id d in
         let (first', middle', midvars') =
           if occur_vars_in_decl env sigma midvars d then
             if not (move_location_eq hto (MoveAfter hyp)) then
-              (first, d :: middle, Id.Set.add hyp midvars)
-            else raise (CannotMoveHyp {from = NamedDecl.get_id declfrom; hto; hyp})
+              (first, (status, d) :: middle, Id.Set.add hyp midvars)
+            else raise (CannotMoveHyp {from = idfrom; hto; hyp})
           else
-            (d::first, middle, midvars)
+            ((status,d)::first, middle, midvars)
         in
         if move_location_eq hto (MoveAfter hyp) then
           push_rev right @@ push middle' @@ push first' ans
@@ -200,19 +207,19 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
   in
   let rec moverec_toright first middle depvars right = match EConstr.match_named_context_val right with
     | None -> push_rev first @@ push_rev middle right
-    | Some (d, _) when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
+    | Some (status, d, _) when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) ->
         push_rev first @@ push_rev middle @@ right
-    | Some (d, right) ->
+    | Some (status, d, right) ->
         let hyp = NamedDecl.get_id d in
         let (first', middle', depvars') =
           if Id.Set.mem hyp depvars then
             if not (move_location_eq hto (MoveAfter hyp)) then
               let vars = global_vars_set_of_decl env sigma d in
               let depvars = Id.Set.union vars depvars in
-              (first, d::middle, depvars)
-            else raise (CannotMoveHyp {from = NamedDecl.get_id declfrom; hto; hyp})
+              (first, (status, d)::middle, depvars)
+            else raise (CannotMoveHyp {from = idfrom; hto; hyp})
           else
-            (d::first, middle, depvars)
+            ((status,d)::first, middle, depvars)
         in
         if move_location_eq hto (MoveAfter hyp) then
           push_rev first' @@ push_rev middle' @@ right
@@ -220,10 +227,9 @@ let move_hyp env sigma toleft (left,declfrom,right) hto =
           moverec_toright first' middle' depvars' right
   in
   if toleft then
-    let id = NamedDecl.get_id declfrom in
-    moverec_toleft right [] [declfrom] (Id.Set.singleton id) left
+    moverec_toleft right [] [declfrom] (Id.Set.singleton idfrom) left
   else
-    let depvars = global_vars_set_of_decl env sigma declfrom in
+    let depvars = global_vars_set_of_decl env sigma (snd declfrom) in
     let right = moverec_toright [] [declfrom] depvars right in
     push_rev left @@ right
 
@@ -258,6 +264,6 @@ let convert_hyp ~check ~reorder env sigma d =
     if check && not (Option.equal (is_conv env sigma) b c) then
       user_err
         (str "Incorrect change of the body of "++ Id.print id ++ str ".");
-    let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in
+    let sign' = apply_to_hyp sign id (fun _ status _ _ -> status, EConstr.Unsafe.to_named_decl d) in
     if reorder then reorder_val_context env sigma sign' (check_decl_position env sigma sign d)
     else sign'
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 1983c8b6f49f..32a3f92c8b34 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -61,5 +61,5 @@ val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move
   Environ.named_context_val -> Environ.named_context_val
 
 val insert_decl_in_named_context : Environ.env -> Evd.evar_map ->
-  EConstr.named_declaration -> Id.t move_location ->
+  Environ.var_status * EConstr.named_declaration -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 1068d0d94dbd..d7f378482404 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -17,30 +17,38 @@ module NamedDecl = Context.Named.Declaration
 let extract_prefix env info =
   let ctx1 = List.rev (EConstr.named_context env) in
   let ctx2 = List.rev (Evd.evar_context info) in
-  let rec share l1 l2 accu = match l1, l2 with
+  let rec share l1 l2 = match l1, l2 with
   | d1 :: l1, d2 :: l2 ->
-    if d1 == d2 then share l1 l2 (d1 :: accu)
-    else (accu, d2 :: l2)
-  | _ -> (accu, l2)
+    if d1 == d2 then share l1 l2
+    else 1 + List.length l2
+  | _ -> List.length l2
   in
-  share ctx1 ctx2 []
+  share ctx1 ctx2
+
+let rec recheck_hyps n env sigma sign =
+  if n = 0 then sigma
+  else match EConstr.match_named_context_val sign with
+    | None -> assert false
+    | Some (_, decl, sign') ->
+      let sigma = recheck_hyps (n-1) env sigma sign' in
+      let env = Environ.reset_with_named_context sign' env in
+      let t = NamedDecl.get_type decl in
+      let sigma, _ = Typing.sort_of env sigma t in
+      let sigma = match decl with
+        | LocalAssum _ -> sigma
+        | LocalDef (_,body,_) -> Typing.check env sigma body t
+      in
+      sigma
 
 let typecheck_evar ev env sigma =
   let info = Evd.find_undefined sigma ev in
+  (* optim: avoid checking unchanged hyps *)
+  let changed = extract_prefix env info in
   (* Typecheck the hypotheses. *)
-  let type_hyp (sigma, env) decl =
-    let t = NamedDecl.get_type decl in
-    let sigma, _ = Typing.sort_of env sigma t in
-    let sigma = match decl with
-    | LocalAssum _ -> sigma
-    | LocalDef (_,body,_) -> Typing.check env sigma body t
-    in
-    (sigma, EConstr.push_named decl env)
-  in
-  let (common, changed) = extract_prefix env info in
-  let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
-  let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
+  let sign = Evd.evar_hyps info in
+  let sigma = recheck_hyps changed env sigma sign in
   (* Typecheck the conclusion *)
+  let env = Environ.reset_with_named_context sign env in
   let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
   sigma
 
diff --git a/proofs/subproof.ml b/proofs/subproof.ml
index b4af1fa69769..ca1f9b1b24b7 100644
--- a/proofs/subproof.ml
+++ b/proofs/subproof.ml
@@ -139,7 +139,7 @@ let build_constant_by_tactic ~name ~sigma ~env ~sign ~poly typ tac =
 
 let build_by_tactic env ~uctx ~poly ~typ tac =
   let name = Id.of_string "temporary_proof" in
-  let sign = Environ.(val_of_named_context (named_context env)) in
+  let sign = Environ.named_context_val env in
   let sigma = Evd.from_ustate uctx in
   (* status doesn't matter: any given up evars can't be in the body/typ
      (we would get OpenProof exception) and we drop the evar part of the evar map *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 95f62ab1e9c0..a1da48783ef7 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -15,7 +15,6 @@ open Reductionops
 open Typing
 open Tacred
 open Logic
-open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
 
@@ -63,10 +62,8 @@ let pf_get_hyp_typ id gl =
 
 let pf_hyps_types gl =
   let env = Proofview.Goal.env gl in
-  let sign = Environ.named_context env in
-  List.map (function LocalAssum (id,x)
-                    | LocalDef (id,_,x) -> id.Context.binder_name, EConstr.of_constr x)
-            sign
+  let sign = EConstr.named_context env in
+  List.map (fun d -> NamedDecl.get_id d, NamedDecl.get_type d) sign
 
 let pf_last_hyp gl =
   let hyps = Proofview.Goal.hyps gl in
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 7faf77ba3973..417c60dd35ad 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Util
-open Termops
 open EConstr
 
 module NamedDecl = Context.Named.Declaration
@@ -18,23 +17,6 @@ module NamedDecl = Context.Named.Declaration
    the current goal, abstracted with respect to the local signature,
    is solved by tac *)
 
-(** d1 is the section variable in the global context, d2 in the goal context *)
-let interpretable_as_section_decl env sigma d1 d2 =
-  let open Context.Named.Declaration in
-  let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env sigma c1 c2 with
-    | None -> false
-    | Some cstr ->
-      try
-        let _sigma = Evd.add_constraints sigma cstr in
-        true
-      with UGraph.UniverseInconsistency _ | UState.UniversesDiffer -> false
-  in
-  match d2, d1 with
-  | LocalDef _, LocalAssum _ -> false
-  | LocalDef (_,b1,t1), LocalDef (_,b2,t2) ->
-    e_eq_constr_univs sigma b1 b2 && e_eq_constr_univs sigma t1 t2
-  | LocalAssum (_,t1), d2 -> e_eq_constr_univs sigma t1 (NamedDecl.get_type d2)
-
 let name_op_to_name ~name_op ~name suffix =
   match name_op with
   | Some s -> s
@@ -56,11 +38,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     let sign,secsign =
       List.fold_right
         (fun d (s1,s2) ->
-           let id = NamedDecl.get_id d in
-           if mem_named_context_val id section_sign &&
-              interpretable_as_section_decl env sigma (lookup_named_val id section_sign) d
-           then (s1,push_named_context_val d s2)
-           else (Context.Named.add d s1,s2))
+           match Environ.var_status (NamedDecl.get_id d) env with
+           | SecVar -> (s1,push_named_context_val SecVar d s2)
+           | ProofVar -> (Context.Named.add d s1,s2))
         goal_sign (Context.Named.empty, Environ.empty_named_context_val)
     in
     let bad id = match lookup_named_val id section_sign with
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 85ca53b315e9..a5089f9bfb4b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -25,8 +25,8 @@ open Hints
 (**************************************************************************)
 
 let compute_secvars gl =
-  let hyps = Proofview.Goal.hyps gl in
-  secvars_of_hyps hyps
+  let env = Proofview.Goal.env gl in
+  secvars_of_hyps (Environ.named_context_val env)
 
 (* Tell auto not to reuse already instantiated metas in unification (for
    compatibility, since otherwise, apply succeeds more often). *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b4dcceffbf02..e90fe12f0ef3 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -442,12 +442,13 @@ let make_resolve_hyp env sigma st only_classes decl db =
       push_resolves env sigma id db
     else db
 
-let make_hints env sigma (modes,st) only_classes sign =
+let make_hints env sigma (modes,st) only_classes =
   let db = Hint_db.add_modes modes @@ Hint_db.empty st true in
-  List.fold_right
-    (fun hyp hints ->
+  EConstr.fold_named_context
+    (fun _ status hyp hints ->
       let consider =
         not only_classes ||
+        not (status = SecVar) ||
         try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in
             (* Section variable, reindex only if the type changed *)
             not (EConstr.eq_constr sigma (EConstr.of_constr t) (NamedDecl.get_type hyp))
@@ -456,7 +457,7 @@ let make_hints env sigma (modes,st) only_classes sign =
       if consider then
         make_resolve_hyp env sigma st only_classes hyp hints
       else hints)
-    sign db
+    env ~init:db
 
 module Intpart = Unionfind.Make(Evar.Set)(Evar.Map)
 
@@ -498,7 +499,7 @@ module Search = struct
                cached_modes == modes
     then cached_hints
     else
-      let hints = make_hints env sigma mst only_classes sign in
+      let hints = make_hints env sigma mst only_classes in
       autogoal_cache := (cwd, only_classes, sign, modes, hints, qvars); hints
 
   let make_autogoal env sigma mst only_classes dep cut best_effort i =
diff --git a/tactics/eClause.ml b/tactics/eClause.ml
index 35a457dce869..6c735ca93b03 100644
--- a/tactics/eClause.ml
+++ b/tactics/eClause.ml
@@ -80,8 +80,7 @@ let make_evar_clause env sigma ?len t =
       let inst, ctx, args, subst = match inst with
       | None ->
         (* Dummy type *)
-        let hypnaming = VarSet.variables (Global.env ()) in
-        let ctx, _, args, subst = push_rel_context_to_named_context ~hypnaming env sigma mkProp in
+        let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in
         Some (ctx, args, subst), ctx, args, subst
       | Some (ctx, args, subst) -> inst, ctx, args, subst
       in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2340da4f8b35..9ac982f17467 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -210,7 +210,7 @@ module Search = struct
     let concl = Proofview.Goal.concl gl in
     let hyps = EConstr.named_context env in
     let db = db env sigma in
-    let secvars = secvars_of_hyps hyps in
+    let secvars = secvars_of_hyps (Environ.named_context_val env) in
     let assumption_tacs =
       let mkdb env sigma = assert false in (* no goal can be generated *)
       let map_assum id = (false, mkdb, e_give_exact (mkVar id), lazy (str "exact" ++ spc () ++ Id.print id)) in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 77431b5a7e45..9292bed8a0a8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1186,7 +1186,7 @@ let discr_positions env sigma { eq_data = (_, _ , s, (t, _, _)) as eq_data; eq_t
   let false_ty = Retyping.get_type_of env sigma false_0 in
   let false_kind = Retyping.get_sort_of env sigma false_0 in
   let e = next_ident_away eq_baseid (vars_of_env env) in
-  let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e ERelevance.relevant,t)) env in
+  let e_env = push_named ProofVar (LocalAssum (make_annot e ERelevance.relevant,t)) env in
 
   let discriminator =
     try
@@ -1415,7 +1415,7 @@ let simplify_args env sigma t =
 let inject_at_positions env sigma l2r eq posns tac =
   let { eq_data = (eq, congr, s, (t,t1,t2)); eq_term = v; eq_evar = evs } = eq in
   let e = next_ident_away eq_baseid (vars_of_env env) in
-  let e_env = push_named (LocalAssum (make_annot e ERelevance.relevant,t)) env in
+  let e_env = push_named ProofVar (LocalAssum (make_annot e ERelevance.relevant,t)) env in
   let evdref = ref sigma in
   let filter (cpath, t1', t2') =
     try
@@ -1849,7 +1849,7 @@ let subst_one_var dep_proof_ok x =
             (str "Cannot find any non-recursive equality over " ++ Id.print x ++
                str".")
         with FoundHyp res -> res in
-      if is_section_variable (Global.env ()) x then
+      if is_section_variable_env env x then
         check_non_indirectly_dependent_section_variable gl x;
       subst_one dep_proof_ok x res
   end
diff --git a/tactics/fixTactics.ml b/tactics/fixTactics.ml
index 4b44217c33eb..a2179cf62420 100644
--- a/tactics/fixTactics.ml
+++ b/tactics/fixTactics.ml
@@ -55,7 +55,7 @@ let mutual_fix f n others = Proofview.Goal.enter begin fun gl ->
     let ()  = check_mutind env sigma n ar in
     if mem_named_context_val f sign then
       TacticErrors.intro_already_declared f;
-    mk_sign (push_named_context_val (LocalAssum (make_annot f r, ar)) sign) oth
+    mk_sign (push_named_context_val ProofVar (LocalAssum (make_annot f r, ar)) sign) oth
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
   Refine.refine ~typecheck:false begin fun sigma ->
@@ -98,7 +98,7 @@ let mutual_cofix f others = Proofview.Goal.enter begin fun gl ->
     let open Context.Named.Declaration in
     if mem_named_context_val f sign then
       TacticErrors.already_used f;
-    mk_sign (push_named_context_val (LocalAssum (make_annot f r, ar)) sign) oth
+    mk_sign (push_named_context_val ProofVar (LocalAssum (make_annot f r, ar)) sign) oth
   in
   let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in
   Refine.refine ~typecheck:false begin fun sigma ->
diff --git a/tactics/generalize.ml b/tactics/generalize.ml
index 31460e3a7684..efabb5313b1d 100644
--- a/tactics/generalize.ml
+++ b/tactics/generalize.ml
@@ -152,7 +152,8 @@ let generalize_dep ?(with_let=false) c =
   let sigma = Proofview.Goal.sigma gl in
   let concl = Proofview.Goal.concl gl in
   let sign = named_context_val env in
-  let init_ids = ids_of_named_context (Global.named_context()) in
+  (* XXX avoid section variables still in env instead of all section variables? *)
+  let init_ids = Environ.ids_of_named_context_val (Global.named_context_val()) in
   let seek (d:named_declaration) (toquant:named_context) =
     if List.exists (fun d' -> occur_var_in_decl env sigma (NamedDecl.get_id d') d) toquant
       || dependent_in_decl sigma c d then
@@ -161,10 +162,10 @@ let generalize_dep ?(with_let=false) c =
       toquant in
   let to_quantify = Context.Named.fold_outside seek (named_context_of_val sign) ~init:[] in
   let qhyps = List.map NamedDecl.get_id to_quantify in
-  let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
+  let tothin = List.filter (fun id -> not (Id.Set.mem id init_ids)) qhyps in
   let tothin' =
     match EConstr.kind sigma c with
-      | Var id when mem_named_context_val id sign && not (Id.List.mem id init_ids)
+      | Var id when mem_named_context_val id sign && not (Id.Set.mem id init_ids)
           -> tothin@[id]
       | _ -> tothin
   in
@@ -172,7 +173,7 @@ let generalize_dep ?(with_let=false) c =
   let is_var, body = match EConstr.kind sigma c with
   | Var id ->
     let body = NamedDecl.get_value (Tacmach.pf_get_hyp id gl) in
-    let is_var = Option.is_empty body && not (List.mem id init_ids) in
+    let is_var = Option.is_empty body && not (Id.Set.mem id init_ids) in
     if with_let then is_var, body else is_var, None
   | _ -> false, None
   in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 540f435732d8..698af4e61d68 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -77,14 +77,13 @@ let secvars_of_hyps hyps =
   let open Context.Named.Declaration in
   let pred, all =
     List.fold_left (fun (pred,all) decl ->
-        try let _ = Context.Named.lookup (get_id decl) hyps in
-          (* Approximation, it might be an hypothesis reintroduced with same name and unconvertible types,
-             we must allow it currently, as comparing the declarations for syntactic equality is too
-             strong a check (e.g. an unfold in a section variable would make it unusable). *)
+        if Termops.is_section_variable_sign ~check:false hyps (get_id decl) then
           (Id.Pred.add (get_id decl) pred, all)
-        with Not_found -> (pred, false))
+        else (pred, false))
       (Id.Pred.empty,true) secctx
   in
+  (* NB: this is not just [forall is_secvar hyps] because we need to
+     know if secvars have been cleaned *)
   if all then Id.Pred.full (* If the whole section context is available *)
   else pred
 
@@ -895,14 +894,16 @@ let error_no_such_hint_database x =
 
 let with_uid c = { obj = c; uid = fresh_key () }
 
-let secvars_of_idset s =
+(* if [x] is a local variable sharing a name with a cleared section
+   variable, [secvars_of_global _ (VarRef x)] should return the empty set *)
+let secvars_of_idset env s =
   Id.Set.fold (fun id p ->
-      if is_section_variable (Global.env ()) id then
+      if is_section_variable_env env id then
         Id.Pred.add id p
       else p) s Id.Pred.empty
 
 let secvars_of_global env gr =
-  secvars_of_idset (vars_of_global env gr)
+  secvars_of_idset env (vars_of_global env gr)
 
 let fresh_global_hint env sigma gr =
   let (c, ctx) = UnivGen.fresh_global_instance env gr in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 568fb4cd754a..da7bdae78c6b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -23,7 +23,7 @@ val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array
 
 type debug = Debug | Info | Off
 
-val secvars_of_hyps : ('c, 't,'r) Context.Named.pt -> Id.Pred.t
+val secvars_of_hyps : Environ.named_context_val -> Id.Pred.t
 
 val empty_hint_info : 'a Typeclasses.hint_info_gen
 
diff --git a/tactics/induction.ml b/tactics/induction.ml
index 553fcdfdbfeb..191708085726 100644
--- a/tactics/induction.ml
+++ b/tactics/induction.ml
@@ -216,10 +216,10 @@ let insert_before decls lasthyp env =
   | None -> push_named_context decls env
   | Some id ->
   Environ.fold_named_context
-    (fun _ d env ->
+    (fun _ status d env ->
       let d = EConstr.of_named_decl d in
       let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in
-      push_named d env)
+      push_named status d env)
     ~init:(reset_context env) env
 
 let mk_eq_name env id {CAst.loc;v=ido} =
@@ -237,8 +237,8 @@ let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
   let open Context.Named.Declaration in
   let t = match ty with Some t -> t | _ -> typ_of env sigma c in
   let r = Retyping.relevance_of_type env sigma t in
-  let decl = if dep then LocalDef (make_annot id r,c,t)
-             else LocalAssum (make_annot id r,t)
+  let decl = if dep then LocalDef (make_annot id r, c, t)
+    else LocalAssum (make_annot id r, t)
   in
   match with_eq with
   | Some (lr,heq) ->
@@ -251,13 +251,13 @@ let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
       let sigma, eq = Typing.checked_applist env sigma eq [t] in
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
-      let newenv = insert_before [LocalAssum (make_annot heq ERelevance.relevant,eq); decl] lastlhyp env in
+      let newenv = insert_before [ProofVar, LocalAssum (make_annot heq ERelevance.relevant,eq); ProofVar, decl] lastlhyp env in
       let (sigma, x) = new_evar newenv sigma ccl in
       (sigma, mkNamedLetIn sigma (make_annot id r) c t
          (mkNamedLetIn sigma (make_annot heq ERelevance.relevant) refl eq x),
       Some (fst @@ destEvar sigma x))
   | None ->
-      let newenv = insert_before [decl] lastlhyp env in
+      let newenv = insert_before [ProofVar, decl] lastlhyp env in
       let (sigma, x) = new_evar newenv sigma ccl in
       (sigma, mkNamedLetIn sigma (make_annot id r) c t x, Some (fst @@ destEvar sigma x))
 
@@ -589,8 +589,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma =
   let lstatus = ref [] in
   let before = ref true in
   let maindep = ref false in
-  let seek_deps env decl rhyp =
-    let decl = EConstr.of_named_decl decl in
+  let seek_deps env _ decl rhyp =
     let hyp = NamedDecl.get_id decl in
     if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false)
     then begin
@@ -1398,7 +1397,7 @@ let induction_gen ~clear_flag ~isrec ~with_evars elim
   let cls = Option.default allHypsAndConcl cls in
   let t = typ_of env evd c in
   let is_arg_pure_hyp =
-    isVar evd c && not (mem_named_context_val (destVar evd c) (Global.named_context_val ()))
+    isVar evd c && not (is_section_variable_env env (destVar evd c))
     && lbind == NoBindings && not with_evars && Option.is_empty eqname
     && clear_flag == None
     && has_generic_occurrences_but_goal cls (destVar evd c) env evd ccl in
@@ -1446,28 +1445,27 @@ let induction_gen_l isrec with_evars elim names lc =
     match l with
       | [] -> Proofview.tclUNIT ()
       | c::l' ->
-          Proofview.tclEVARMAP >>= fun sigma ->
+        Proofview.Goal.enter begin fun gl ->
+          let env = Proofview.Goal.env gl in
+          let sigma = Proofview.Goal.sigma gl in
           match EConstr.kind sigma c with
-            | Var id when not (mem_named_context_val id (Global.named_context_val ()))
-                && not with_evars ->
-                let () = newlc:= id::!newlc in
-                atomize_list l'
-
-            | _ ->
-                Proofview.Goal.enter begin fun gl ->
-                let env = Proofview.Goal.env gl in
-                let sigma = Proofview.Goal.sigma gl in
-                let sigma, t = Typing.type_of env sigma c in
-                let x = id_of_name_using_hdchar env sigma t Anonymous in
-                let id = new_fresh_id Id.Set.empty x gl in
-                let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
-                let () = newlc:=id::!newlc in
-                Tacticals.tclTHENLIST [
-                  tclEVARS sigma;
-                  Tactics.letin_tac None (Name id) c None allHypsAndConcl;
-                  atomize_list newl';
-                ]
-                end in
+          | Var id when not (is_section_variable_env env id)
+                     && not with_evars ->
+            let () = newlc:= id::!newlc in
+            atomize_list l'
+
+          | _ ->
+            let sigma, t = Typing.type_of env sigma c in
+            let x = id_of_name_using_hdchar env sigma t Anonymous in
+            let id = new_fresh_id Id.Set.empty x gl in
+            let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in
+            let () = newlc:=id::!newlc in
+            Tacticals.tclTHENLIST [
+              tclEVARS sigma;
+              Tactics.letin_tac None (Name id) c None allHypsAndConcl;
+              atomize_list newl';
+            ]
+        end in
   Tacticals.tclTHENLIST
     [
       (atomize_list lc);
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c2011de9df77..24276be57f82 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -838,7 +838,7 @@ let resolve_morphism env m args args' (b,cstr) evars =
     let _, dosub = app_poly_sort b env evars dosub [||] in
     let _, appsub = app_poly_nocheck env evars appsub [||] in
     let dosub_id = Id.of_string "do_subrelation" in
-    let env' = EConstr.push_named (LocalDef (make_annot dosub_id ERelevance.relevant, dosub, appsub)) env in
+    let env' = EConstr.push_named ProofVar (LocalDef (make_annot dosub_id ERelevance.relevant, dosub, appsub)) env in
     let evars, morph = new_cstr_evar evars env' app in
     (* Replace the free [dosub_id] in the evar by the global reference *)
     let morph = Vars.replace_vars (fst evars) [dosub_id , dosub] morph in
@@ -1745,8 +1745,8 @@ let cl_rewrite_clause_newtac ?origsigma ~progress abs strat clause =
     | None -> env
     | Some id ->
       (* Only consider variables not depending on [id] *)
-      let ctx = named_context env in
-      let filter decl = not (occur_var_in_decl env sigma id decl) in
+      let ctx = named_context_of_val_with_status @@ named_context_val env in
+      let filter (_, decl) = not (occur_var_in_decl env sigma id decl) in
       let nctx = List.filter filter ctx in
       Environ.reset_with_named_context (val_of_named_context nctx) env
     in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 907bceb5051b..0ad37135dc2e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -81,8 +81,8 @@ let () =
 let unsafe_intro env decl ~relevance b =
   Refine.refine_with_principal ~typecheck:false begin fun sigma ->
     let ctx = named_context_val env in
-    let nctx = push_named_context_val decl ctx in
-    let inst = EConstr.identity_subst_val (named_context_val env) in
+    let nctx = push_named_context_val ProofVar decl ctx in
+    let inst = EConstr.identity_subst_val ctx in
     let ninst = SList.cons (mkRel 1) inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
     let (sigma, ev) = new_pure_evar nctx sigma ~relevance nb in
@@ -156,15 +156,25 @@ end
 let convert x y = convert_gen Conversion.CONV x y
 let convert_leq x y = convert_gen Conversion.CUMUL x y
 
+(* this should be an error but random code relies on it, eg
+   "match goal with H : _ |- _ => destruct H; clear H end" *)
+let warn_clear_nohyp = CWarnings.create ~name:"clear-no-such-hyp" ~category:CWarnings.CoreCategories.tactics
+    Pp.(fun id -> fmt "No such hypothesis: %t." (fun () -> Id.print id))
+
 let clear_gen fail = function
 | [] -> Proofview.tclUNIT ()
 | ids ->
   Proofview.Goal.enter begin fun gl ->
-    let ids = List.fold_right Id.Set.add ids Id.Set.empty in
-    (* clear_hyps_in_evi does not require nf terms *)
     let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let concl = Proofview.Goal.concl gl in
+    let add id acc =
+      if Environ.mem_named id env then Id.Set.add id acc
+      else
+        let () = warn_clear_nohyp id in
+        acc
+    in
+    let ids = List.fold_right add ids Id.Set.empty in
     let (sigma, hyps, concl) =
       try clear_hyps_in_evi env sigma (named_context_val env) concl ids
       with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal
@@ -217,6 +227,74 @@ let move_hyp id dest =
     end
   end
 
+let error_renaming_implicit_dependency ?loc env where ids gr =
+  CErrors.user_err ?loc @@
+  fmt "Cannot rename section variable %t@ because it is used implicitly through %t@ in %t."
+    (fun () -> Id.print (Id.Set.choose ids))
+    (fun () -> pr_global_env env gr)
+    (fun () -> match where with
+       | None -> str "the conclusion"
+       | Some h -> fmt "hypothesis %t" (fun () -> Id.print h))
+
+let check_renaming ~src ~dst env sigma concl =
+  let sign = named_context_val env in
+  (* Check that we do not mess variables *)
+  let vars = ids_of_named_context_val sign in
+  let () =
+    if not (Id.Set.subset src vars) then
+      let hyp = Id.Set.choose (Id.Set.diff src vars) in
+      raise (RefinerError (env, sigma, NoSuchHyp hyp))
+  in
+  let mods = Id.Set.diff vars src in
+  let () =
+    try
+      let elt = Id.Set.choose (Id.Set.inter dst mods) in
+      TacticErrors.already_used elt
+    with Not_found -> ()
+  in
+  let secvars =
+    Id.Set.filter (fun id ->
+        match var_status id env with
+        | SecVar -> true
+        | ProofVar -> false)
+      src
+  in
+  let checked = ref GlobRef.Set_env.empty in
+  let check_constr where c =
+    let rec aux c =
+      match EConstr.destRef sigma c with
+      | VarRef _, _ ->
+        (* we only refuse implicit dependencies, because they can't be substituted *)
+        ()
+      | gr, _ ->
+        if GlobRef.Set_env.mem gr !checked then ()
+        else begin
+          let deps = Evarutil.vars_of_global env sigma gr in
+          let bad = Id.Set.inter deps secvars in
+          let () =
+            if not @@ Id.Set.is_empty bad then
+              error_renaming_implicit_dependency env where bad gr
+          in
+          checked := GlobRef.Set_env.add gr !checked
+        end
+      | exception DestKO -> EConstr.iter sigma aux c
+    in
+    aux c
+  in
+  let () =
+    if Id.Set.is_empty secvars then
+      (* not renaming any secvars -> no problem *)
+      ()
+    else
+      let () = check_constr None concl in
+      let () =
+        List.iter (fun d -> NamedDecl.iter_constr (check_constr (Some (NamedDecl.get_id d))) d)
+          (named_context env)
+      in
+      ()
+  in
+  ()
+
 let rename_hyp repl =
   let fold accu (src, dst) = match accu with
   | None -> None
@@ -238,34 +316,24 @@ let rename_hyp repl =
     Proofview.Goal.enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let env = Proofview.Goal.env gl in
-      let sign = named_context_val env in
       let sigma = Proofview.Goal.sigma gl in
       let relevance = Proofview.Goal.relevance gl in
-      (* Check that we do not mess variables *)
-      let vars = ids_of_named_context_val sign in
-      let () =
-        if not (Id.Set.subset src vars) then
-          let hyp = Id.Set.choose (Id.Set.diff src vars) in
-          raise (RefinerError (env, sigma, NoSuchHyp hyp))
-      in
-      let mods = Id.Set.diff vars src in
-      let () =
-        try
-          let elt = Id.Set.choose (Id.Set.inter dst mods) in
-          TacticErrors.already_used elt
-        with Not_found -> ()
-      in
+      let () = check_renaming ~src ~dst env sigma concl in
       (* All is well *)
       let make_subst (src, dst) = (src, mkVar dst) in
       let subst = List.map make_subst repl in
       let subst c = Vars.replace_vars sigma subst c in
-      let replace id = try List.assoc_f Id.equal id repl with Not_found -> id in
-      let map decl = decl |> NamedDecl.map_id replace |> NamedDecl.map_constr subst in
-      let ohyps = named_context_of_val sign in
+      let map (status, decl) =
+        let decl = NamedDecl.map_constr subst decl in
+        match List.assoc_f_opt Id.equal (NamedDecl.get_id decl) repl with
+        | None -> status, decl
+        | Some id -> ProofVar, NamedDecl.set_id id decl
+      in
+      let ohyps = EConstr.named_context_of_val_with_status @@ Environ.named_context_val env in
       let nhyps = List.map map ohyps in
       let nconcl = subst concl in
       let nctx = val_of_named_context nhyps in
-      let fold odecl ndecl accu =
+      let fold (_,odecl) (_,ndecl) accu =
         if Id.equal (NamedDecl.get_id odecl) (NamedDecl.get_id ndecl) then
           SList.default accu
         else
@@ -379,12 +447,12 @@ let internal_cut ?(check=true) replace id t =
       if replace then
         let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in
         let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in
-        let sign' = insert_decl_in_named_context env sigma (LocalAssum (make_annot id r,t)) nexthyp sign' in
+        let sign' = insert_decl_in_named_context env sigma (ProofVar,LocalAssum (make_annot id r,t)) nexthyp sign' in
         Environ.reset_with_named_context sign' env,t,concl,sigma
       else
         (if check && mem_named_context_val id sign then
           TacticErrors.intro_already_declared id;
-         push_named (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in
+         push_named ProofVar (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in
     let nf_t = nf_betaiota env sigma t in
     Proofview.tclTHEN
       (Proofview.Unsafe.tclEVARS sigma)
@@ -443,6 +511,7 @@ let[@ocaml.inline] (let*) m f = match m with
 | NoChange -> NoChange
 | Changed v -> f v
 
+(* should secvar status change when Changed? *)
 let e_pf_change_decl (redfun : bool -> Tacred.change_function) where env sigma decl =
   let open Context.Named.Declaration in
   match decl with
@@ -531,7 +600,7 @@ let e_change_in_hyps ~check ~reorder f args = match args with
       in
       let reds = List.fold_left fold Id.Map.empty args in
       let evdref = ref sigma in
-      let map d =
+      let map status d =
         let id = NamedDecl.get_id d in
         match Id.Map.find id reds with
         | reds ->
@@ -542,8 +611,8 @@ let e_change_in_hyps ~check ~reorder f args = match args with
           in
           let (sigma, d) = List.fold_right fold reds (sigma, d) in
           let () = evdref := sigma in
-          EConstr.Unsafe.to_named_decl d
-        | exception Not_found -> d
+          status, EConstr.Unsafe.to_named_decl d
+        | exception Not_found -> status, d
       in
       let sign = Environ.map_named_val map (Environ.named_context_val env) in
       let env = reset_with_named_context sign env in
@@ -947,7 +1016,7 @@ let intro_forthcoming_last_then_gen avoid dep_flag bound n tac =
     if List.is_empty ids then tac []
     else Refine.refine_with_principal ~typecheck:false begin fun sigma ->
       let ctx = named_context_val env in
-      let nctx = List.fold_right push_named_context_val ndecls ctx in
+      let nctx = List.fold_right (fun d ctx -> push_named_context_val ProofVar d ctx) ndecls ctx in
       let inst = SList.defaultn (List.length @@ Environ.named_context env) SList.empty in
       let rels = List.init (List.length decls) (fun i -> mkRel (i + 1)) in
       let ninst = List.fold_right (fun c accu -> SList.cons c accu) rels inst in
@@ -1916,7 +1985,7 @@ let clear_body idl =
     let env = Proofview.Goal.env gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Proofview.Goal.sigma gl in
-    let ctx = named_context env in
+    let ctx = named_context_of_val_with_status (named_context_val env) in
     let ids = Id.Set.of_list idl in
     let () =
       match Id.Set.find_first_opt (fun v -> not (mem_named v env)) ids with
@@ -1932,7 +2001,7 @@ let clear_body idl =
       else
         match ctx with
         | [] -> assert false
-        | decl :: ctx ->
+        | (status, decl) :: ctx ->
           let decl, ids, found =
             match decl with
             | LocalAssum (id,t) ->
@@ -1950,9 +2019,9 @@ let clear_body idl =
           if Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) ids then
             let sigma = check_decl env sigma idl ids decl in (* can sigma really change? *)
             let ids = Id.Set.add (get_id decl) ids in
-            push_named decl env, sigma, Id.Set.add (get_id decl) ids
+            push_named status decl env, sigma, Id.Set.add (get_id decl) ids
           else
-            push_named decl env, sigma, if found then Id.Set.add (get_id decl) ids else ids
+            push_named status decl env, sigma, if found then Id.Set.add (get_id decl) ids else ids
     in
     try
       let env, sigma, ids = fold ids ctx in
@@ -2534,7 +2603,7 @@ let pose_tac na c =
     Proofview.Unsafe.tclEVARS sigma <*>
     Refine.refine ~typecheck:false begin fun sigma ->
       let id = make_annot id rel in
-      let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
+      let nhyps = EConstr.push_named_context_val ProofVar (NamedDecl.LocalDef (id, c, t)) hyps in
       let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma ~relevance concl in
       let inst = EConstr.identity_subst_val hyps in
       let body = mkEvar (ev, SList.cons (mkRel 1) inst) in
diff --git a/test-suite/bugs/bug_11487.v b/test-suite/bugs/bug_11487.v
new file mode 100644
index 000000000000..886009670efc
--- /dev/null
+++ b/test-suite/bugs/bug_11487.v
@@ -0,0 +1,16 @@
+Parameter parameters: Type.
+Parameter mem: parameters -> Type.
+Parameter rel: forall {p: parameters}, mem p -> mem p -> Prop.
+
+Section Foo.
+  Context (p: parameters).
+
+  Lemma Proper_load: forall (m: mem p), rel m m. Admitted.
+
+  Goal forall (p: parameters) (m: mem p), rel m m.
+  Proof.
+    clear p.
+    intros p m.
+    Fail Check Proper_load.
+  Abort.
+End Foo.
diff --git a/test-suite/bugs/bug_12304.v b/test-suite/bugs/bug_12304.v
new file mode 100644
index 000000000000..2f2740ffe607
--- /dev/null
+++ b/test-suite/bugs/bug_12304.v
@@ -0,0 +1,11 @@
+Section S.
+Variable a:nat.
+Definition b:=a.
+Goal b=b.
+Proof.
+  Fail rename a into c.
+  generalize b. intros b.
+  rename a into c.
+  Fail unfold b.
+Abort.
+End S.
diff --git a/test-suite/bugs/bug_18858.v b/test-suite/bugs/bug_18858.v
new file mode 100644
index 000000000000..a2f6b4df79a0
--- /dev/null
+++ b/test-suite/bugs/bug_18858.v
@@ -0,0 +1,9 @@
+Section Test.
+ Context (H : True).
+ Goal True /\ True -> True.
+ Proof.
+   intros H'. rename H into H0. rename H' into H.
+   repeat match goal with [ H : _ /\ _ |- _ ] => destruct H end. (* fails with timeout because [H] is not cleared by [destruct] *)
+   trivial.
+ Qed.
+End Test.
diff --git a/test-suite/bugs/bug_20847_1.v b/test-suite/bugs/bug_20847_1.v
new file mode 100644
index 000000000000..0937bed6a388
--- /dev/null
+++ b/test-suite/bugs/bug_20847_1.v
@@ -0,0 +1,18 @@
+(* #20847 is about secvars not getting renamed when pushing rel to
+   named.
+
+   This test checks that clearing a secvar and renaming some other var
+   to reuse the secvar name is correctly handled (which seems
+   necessary to handle renaming secvars in the future). *)
+Section C.
+  Variable n : nat.
+
+  Definition d : n = n := eq_refl.
+
+  Lemma l : n = n.
+  Proof.
+    revert n; intros []; [ reflexivity | ].
+    apply eq_S. Fail apply d.
+  Fail Qed.
+  Abort.
+End C.
diff --git a/test-suite/bugs/bug_21987_1.v b/test-suite/bugs/bug_21987_1.v
new file mode 100644
index 000000000000..c67a26644c26
--- /dev/null
+++ b/test-suite/bugs/bug_21987_1.v
@@ -0,0 +1,16 @@
+
+Axiom t : Type -> Type.
+
+Section S.
+  Variable elt : Type.
+
+  Lemma t_ind :
+   forall P : t elt -> Type,
+   forall m, P m.
+  Proof.
+  Admitted.
+
+  Goal forall m : t elt, m = m.
+    induction m using t_ind.
+  Qed.
+End S.
diff --git a/test-suite/bugs/bug_21987_2.v b/test-suite/bugs/bug_21987_2.v
new file mode 100644
index 000000000000..557bef096d3d
--- /dev/null
+++ b/test-suite/bugs/bug_21987_2.v
@@ -0,0 +1,8 @@
+Goal True /\ True -> True.
+Proof.
+  intros H.
+  match goal with
+  | H : _ /\ _ |- _ =>
+     destruct H as [H1 H2]; try clear H
+  end.
+Abort.
diff --git a/test-suite/bugs/bug_6773.v b/test-suite/bugs/bug_6773.v
new file mode 100644
index 000000000000..4a8f0dc8095b
--- /dev/null
+++ b/test-suite/bugs/bug_6773.v
@@ -0,0 +1,14 @@
+Section BuggySection.
+
+  Variable B: nat.
+
+  Axiom F: False. (* To replace admits, allowing QED in bug*)
+
+  Lemma BUG (i: nat) : False.
+  Proof.
+    induction i in B.
+    assert (B = B) by abstract reflexivity.
+    all: now destruct F. (* No more subgoals. *)
+  Qed. (* fails *)
+
+End BuggySection.
diff --git a/test-suite/output/SecVar.out b/test-suite/output/SecVar.out
new file mode 100644
index 000000000000..6f32683e6776
--- /dev/null
+++ b/test-suite/output/SecVar.out
@@ -0,0 +1,18 @@
+1 goal
+  
+  a (* section variable *), b (* section variable *) : nat
+  H (* section variable *) : a = b
+  ============================
+  True
+1 goal
+  
+  a (* section variable *), b (* section variable *) : nat
+  H (* hypothesis *) : b = a
+  ============================
+  True
+1 goal
+  
+  a (* section variable *), y (* hypothesis *) : nat
+  H (* hypothesis *) : y = a
+  ============================
+  True
diff --git a/test-suite/output/SecVar.v b/test-suite/output/SecVar.v
new file mode 100644
index 000000000000..82116643fa3a
--- /dev/null
+++ b/test-suite/output/SecVar.v
@@ -0,0 +1,15 @@
+Section S.
+  Variables a b : nat.
+  Variable H : a = b.
+
+  Set Printing Variables Status.
+
+  Goal True.
+  Proof.
+    Show.
+    apply eq_sym in H.
+    Show.
+    rename b into y.
+    Show.
+  Abort.
+End S.
diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v
index 03034cf1305e..ad093ef6b9bb 100644
--- a/test-suite/success/clear.v
+++ b/test-suite/success/clear.v
@@ -15,19 +15,34 @@ Qed.
 
 Class A.
 
+Class B := BB : A.
+
 Section Foo.
 
   Variable a : A.
 
   Goal A.
     solve [typeclasses eauto].
-    Undo 1.
+  Qed.
+
+  Goal A.
     clear a.
-    try typeclasses eauto.
+    Fail solve [ typeclasses eauto ].
     assert(a:=Build_A).
     solve [ typeclasses eauto ].
-    Undo 2.
+  Qed.
+
+  Goal A.
+    clear a.
     assert(b:=Build_A).
     solve [ typeclasses eauto ].
   Qed.
+
+  Instance myb : B := a.
+
+  Goal B.
+    clear a.
+    assert(a:=Build_A).
+    Fail solve [typeclasses eauto].
+  Abort.
 End Foo.
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 8af3fa4a8822..dccd0d827cda 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -452,7 +452,7 @@ let interp_mutual_definition env ~program_mode ~poly ~function_mode rec_order fi
     List.fold_left4
       (fun (sigma, rec_sign) id r t (_,extradecl) ->
          let sigma, r, t = if program_mode && List.is_empty extradecl then encapsulate env sigma r t else sigma, r, t in
-         sigma, LocalAssum (Context.make_annot id r, t) :: rec_sign)
+         sigma, (Environ.ProofVar, LocalAssum (Context.make_annot id r, t)) :: rec_sign)
       (sigma, []) fixnames fixrs fixtypes fixextras
   in
   let fixrecimps = List.map3 (fun ctximps wfimps cclimps -> ctximps @ wfimps @ cclimps) fixctximps fixwfimps fixcclimps in
@@ -470,7 +470,7 @@ let interp_mutual_definition env ~program_mode ~poly ~function_mode rec_order fi
         (fun sigma fixctximpenv (after,extradecl) ctx body ccl ->
            let impls = Id.Map.fold Id.Map.add fixctximpenv impls in
            let env', ctx =
-             if after then env, List.map NamedDecl.to_rel_decl rec_sign @ ctx
+             if after then env, List.map (fun (_,d) -> NamedDecl.to_rel_decl d) rec_sign @ ctx
              else push_named_context rec_sign env, extradecl@ctx in
            interp_fix_body ~program_mode env' ctx sigma impls body (Vars.lift (Context.Rel.length extradecl) ccl))
         sigma fixctximpenvs fixextras fixctxs fixl fixccls)
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 8bc033f82fa2..a7fa69557df4 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1832,7 +1832,7 @@ let initialize_named_context_for_proof () =
     (fun d signv ->
       let id = NamedDecl.get_id d in
       let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in
-      Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
+      Environ.push_named_context_val SecVar d signv) sign Environ.empty_named_context_val
 
 let start_proof_core ~name ~pinfo ?using sigma goals =
   (* In ?sign, we remove the bodies of variables in the named context
@@ -1919,7 +1919,7 @@ let start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma =
     let sign =
       List.fold_left2 (fun sign CInfo.{name;typ} r ->
           let decl = Context.Named.Declaration.LocalAssum (Context.make_annot name r, typ) in
-          EConstr.push_named_context_val decl sign) (initialize_named_context_for_proof ()) cinfo' fixrs in
+          EConstr.push_named_context_val ProofVar decl sign) (initialize_named_context_for_proof ()) cinfo' fixrs in
     let using = Option.map (interp_proof_using_cinfo env sigma cinfo') using in
     let goals = List.map (function CInfo.{typ} -> (Some sign, typ)) thms in
     let lemma = start_proof_core ~name ~pinfo ?using sigma goals in
@@ -1929,7 +1929,9 @@ let start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma =
       (* Temporary declaration of notations for the time of the proofs *)
       let ntn_env =
         (* We simulate the goal context in which the fixpoint bodies have to be proved (exact relevance does not matter) *)
-        let make_decl CInfo.{name; typ} = Context.Named.Declaration.LocalAssum (Context.annotR name, typ) in
+        let make_decl CInfo.{name; typ} =
+          Environ.ProofVar, Context.Named.Declaration.LocalAssum (Context.annotR name, typ)
+        in
         Environ.push_named_context (List.map make_decl cinfo) (Global.env()) in
       List.iter (Metasyntax.add_notation_interpretation ~local:(info.scope=Locality.Discharge) ntn_env) info.ntns in
     lemma
@@ -1955,7 +1957,7 @@ let start_mutual_definitions_refine ~info ~cinfo ~bodies ~possible_guard ?using
     let sign =
       List.fold_left2 (fun sign CInfo.{name;typ} r ->
           let decl = Context.Named.Declaration.LocalAssum (Context.make_annot name r, typ) in
-          EConstr.push_named_context_val decl sign) (initialize_named_context_for_proof ()) cinfo fixrs in
+          EConstr.push_named_context_val ProofVar decl sign) (initialize_named_context_for_proof ()) cinfo fixrs in
     let using = Option.map (interp_proof_using_cinfo env sigma cinfo) using in
     let goals = List.map (function CInfo.{typ} -> (Some sign, typ)) thms in
     let lemma = start_proof_core ~name ~pinfo ?using sigma goals in
@@ -1970,7 +1972,9 @@ let start_mutual_definitions_refine ~info ~cinfo ~bodies ~possible_guard ?using
       (* Temporary declaration of notations for the time of the proofs *)
       let ntn_env =
         (* We simulate the goal context in which the fixpoint bodies have to be proved (exact relevance does not matter) *)
-        let make_decl CInfo.{name; typ} = Context.Named.Declaration.LocalAssum (Context.annotR name, EConstr.Unsafe.to_constr typ) in
+        let make_decl CInfo.{name; typ} =
+          Environ.ProofVar, Context.Named.Declaration.LocalAssum (Context.annotR name, EConstr.Unsafe.to_constr typ)
+        in
         Environ.push_named_context (List.map make_decl cinfo) (Global.env()) in
       List.iter (Metasyntax.add_notation_interpretation ~local:(info.scope=Locality.Discharge) ntn_env) info.ntns in
     lemma
@@ -1986,7 +1990,7 @@ let set_used_variables ps ~using =
   let ctx_set =
     List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in
   let vars_of = Environ.global_vars_set in
-  let aux env entry (ctx, all_safe as orig) =
+  let aux env _status entry (ctx, all_safe as orig) =
     match entry with
     | LocalAssum ({Context.binder_name=x},_) ->
        if Id.Set.mem x all_safe then orig
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 1041122c1307..6e132ff6a603 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -230,9 +230,11 @@ let explain_bad_assumption env sigma j =
   brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++
   str "because this term is not a type."
 
-let explain_reference_variables sigma id c =
-  pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++
-  strbrk " which is not declared in the context."
+let explain_reference_variables env sigma id c =
+  pr_global c ++ strbrk " depends on the section variable " ++ Id.print id ++
+  if Environ.mem_named id env then
+    strbrk " but " ++ Id.print id ++ strbrk " in the current context does not refer to the section variable of the same name."
+  else strbrk " which is not declared in the current context."
 
 let explain_elim_arity env sigma ind c okinds =
   let open EConstr in
@@ -1008,7 +1010,7 @@ let explain_type_error env sigma err =
   | BadAssumption c ->
       explain_bad_assumption env sigma c
   | ReferenceVariables (id,c) ->
-      explain_reference_variables sigma id c
+      explain_reference_variables env sigma id c
   | ElimArity (ind, c, okinds) ->
       explain_elim_arity env sigma ind (Some c) okinds
   | CaseNotInductive cj ->
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index c8f7bc6cc4bb..c9d0366ab786 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -109,7 +109,8 @@ let definition_using env evd ~fixnames ~using ~terms =
 let name_set id expr =
   if Id.equal id all_collection_id then err_redefine_all_collection ();
   if is_known_name id then warn_redefine_collection id;
-  if Termops.is_section_variable (Global.env ()) id then warn_variable_shadowing id;
+  (* but we won't warn if id gets declared as a section variable later *)
+  if Environ.mem_named id (Global.env ()) then warn_variable_shadowing id;
   known_names := (id,expr) :: !known_names
 
 let minimize_hyps env ids =
diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml
index 3afbdbf0c322..d2989166ab54 100644
--- a/vernac/retrieveObl.ml
+++ b/vernac/retrieveObl.ml
@@ -237,6 +237,8 @@ let retrieve_obligations env name evm fs ?deps ?status t ty =
     List.fold_right
       (fun (id, (n, nstr), ev) evs ->
         let hyps = Evd.evar_filtered_context ev in
+        (* XXX ignore vars based on secvar status + names of recursive functions
+           instead of length of global context + number of recursive functions *)
         let hyps = trunc_named_context nc_len hyps in
         let evtyp, deps, transp = etype_of_evar evm evs hyps (Evd.evar_concl ev) in
         let evtyp, hyps, chop =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7d2fea021b73..5e9b897fdea7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -823,7 +823,7 @@ let vernac_enable_notation ~module_local on rule interp flags scope =
 
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
-  if Termops.is_section_variable (Global.env ()) id ||
+  if Environ.mem_named id (Global.env ()) ||
      locality <> Discharge && Nametab.exists_cci (Lib.make_path id) ||
      locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
   then
@@ -1943,14 +1943,6 @@ let () =
       optread  = (fun () -> (Global.typing_flags ()).Declarations.unfold_dep_heuristic);
       optwrite = Global.set_unfold_dep_heuristic }
 
-let () =
-  declare_bool_option
-    { optstage = Summary.Stage.Interp;
-      optdepr  = None;
-      optkey   = ["Printing";"Compact";"Contexts"];
-      optread  = (fun () -> Printer.get_compact_context());
-      optwrite = (fun b -> Printer.set_compact_context b) }
-
 let () =
   declare_int_option
     { optstage = Summary.Stage.Interp;