Keep track of which variables are section variables and use this info to fix bugs

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-}"

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

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

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).

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).

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")
 

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

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:

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

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

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
 

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