Merge PR rocq-prover#7004: Make simple apply obey Opaque directive.

Author: ppedrot

CHANGES

@@ -25,6 +25,9 @@ Tactics
 
 - Deprecated the Implicit Tactic family of commands.
 
+- The `simple apply` tactic now respects the `Opaque` flag when called from
+  Ltac (`auto` still does not respect it).
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from

plugins/ssrmatching/ssrmatching.ml4

@@ -312,20 +312,22 @@ let unif_HO_args env ise0 pa i ca =
 (* for HO evars, though hopefully Miller patterns can pick up some of     *)
 (* those cases, and HO matching will mop up the rest.                     *)
 let flags_FO env =
+  let oracle = Environ.oracle env in
+  let ts = Conv_oracle.get_transp_state oracle in
   let flags =
-    { (Unification.default_no_delta_unify_flags ()).Unification.core_unify_flags
+    { (Unification.default_no_delta_unify_flags ts).Unification.core_unify_flags
       with
         Unification.modulo_conv_on_closed_terms = None;
         Unification.modulo_eta = true;
         Unification.modulo_betaiota = true;
-        Unification.modulo_delta_types = Conv_oracle.get_transp_state (Environ.oracle env)}
+        Unification.modulo_delta_types = ts }
   in
   { Unification.core_unify_flags = flags;
     Unification.merge_unify_flags = flags;
     Unification.subterm_unify_flags = flags;
     Unification.allow_K_in_toplevel_higher_order_unification = false;
     Unification.resolve_evars =
-      (Unification.default_no_delta_unify_flags ()).Unification.resolve_evars
+      (Unification.default_no_delta_unify_flags ts).Unification.resolve_evars
   }
 let unif_FO env ise p c =
   Unification.w_unify env ise Reduction.CONV ~flags:(flags_FO env)

pretyping/unification.ml

@@ -398,8 +398,13 @@ let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with
   modulo_betaiota = false;
 }
 
-let default_no_delta_unify_flags () =
-  let flags = default_no_delta_core_unify_flags () in {
+let default_no_delta_unify_flags ts =
+  let flags = default_no_delta_core_unify_flags () in
+  let flags = { flags with
+                modulo_conv_on_closed_terms = Some ts;
+                modulo_delta_types = ts
+              } in
+  {
   core_unify_flags = flags;
   merge_unify_flags = flags;
   subterm_unify_flags = flags;

pretyping/unification.mli

@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Names
 open Constr
 open EConstr
 open Environ
@@ -40,7 +41,7 @@ val default_core_unify_flags : unit -> core_unify_flags
 val default_no_delta_core_unify_flags : unit -> core_unify_flags
 
 val default_unify_flags : unit -> unify_flags
-val default_no_delta_unify_flags : unit -> unify_flags
+val default_no_delta_unify_flags : transparent_state -> unify_flags
 
 val elim_flags : unit -> unify_flags
 val elim_no_delta_flags : unit -> unify_flags

tactics/tactics.ml

@@ -1637,13 +1637,11 @@ let tclORELSEOPT t k =
       Proofview.tclZERO ~info e
     | Some tac -> tac)
 
-let general_apply with_delta with_destruct with_evars clear_flag
-    {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
+let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
+    clear_flag {CAst.loc;v=(c,lbind : EConstr.constr with_bindings)} =
   Proofview.Goal.enter begin fun gl ->
   let concl = Proofview.Goal.concl gl in
   let sigma = Tacmach.New.project gl in
-  let flags =
-    if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   (* The actual type of the theorem. It will be matched against the
   goal. If this fails, then the head constant will be unfolded step by
   step. *)
@@ -1652,7 +1650,12 @@ let general_apply with_delta with_destruct with_evars clear_flag
     Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
-
+    let ts =
+      if respect_opaque then Conv_oracle.get_transp_state (oracle env)
+      else full_transparent_state
+    in
+    let flags =
+      if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
     let thm_ty0 = nf_betaiota env sigma (Retyping.get_type_of env sigma c) in
     let try_apply thm_ty nprod =
       try
@@ -1718,14 +1721,14 @@ let rec apply_with_bindings_gen b e = function
         (general_apply b b e k cb)
         (apply_with_bindings_gen b e cbl)
 
-let apply_with_delayed_bindings_gen b e l = 
+let apply_with_delayed_bindings_gen b e l =
   let one k {CAst.loc;v=f} =
     Proofview.Goal.enter begin fun gl ->
       let sigma = Tacmach.New.project gl in
       let env = Proofview.Goal.env gl in
       let (sigma, cb) = f env sigma in
 	Tacticals.New.tclWITHHOLES e
-          (general_apply b b e k CAst.(make ?loc cb)) sigma
+          (general_apply ~respect_opaque:(not b) b b e k CAst.(make ?loc cb)) sigma
     end
   in
   let rec aux = function
@@ -1800,21 +1803,25 @@ let apply_in_once_main flags innerclause env sigma (loc,d,lbind) =
   in
   aux (make_clenv_binding env sigma (d,thm) lbind)
 
-let apply_in_once sidecond_first with_delta with_destruct with_evars naming
-    id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
+let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
+    with_destruct with_evars naming id (clear_flag,{ CAst.loc; v= d,lbind}) tac =
   let open Context.Rel.Declaration in
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
-  let flags =
-    if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
   let t' = Tacmach.New.pf_get_hyp_typ id gl in
   let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
   let targetid = find_name true (LocalAssum (Anonymous,t')) naming gl in
   let rec aux idstoclear with_destruct c =
     Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
+    let ts =
+      if respect_opaque then Conv_oracle.get_transp_state (oracle env)
+      else full_transparent_state
+    in
+    let flags =
+      if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
     try
       let clause = apply_in_once_main flags innerclause env sigma (loc,c,lbind) in
       clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
@@ -1834,14 +1841,14 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
   aux [] with_destruct d
   end
 
-let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars naming
-    id (clear_flag,{CAst.loc;v=f}) tac =
+let apply_in_delayed_once ?(respect_opaque = false) sidecond_first with_delta
+    with_destruct with_evars naming id (clear_flag,{CAst.loc;v=f}) tac =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let (sigma, c) = f env sigma in
     Tacticals.New.tclWITHHOLES with_evars 
-      (apply_in_once sidecond_first with_delta with_destruct with_evars
+      (apply_in_once ~respect_opaque sidecond_first with_delta with_destruct with_evars
          naming id (clear_flag,CAst.(make ?loc c)) tac)
       sigma
   end
@@ -2531,11 +2538,11 @@ let assert_as first hd ipat t =
 
 (* apply in as *)
 
-let general_apply_in sidecond_first with_delta with_destruct with_evars
-    id lemmas ipat =
+let general_apply_in ?(respect_opaque=false) sidecond_first with_delta
+    with_destruct with_evars id lemmas ipat =
   let tac (naming,lemma) tac id =
-    apply_in_delayed_once sidecond_first with_delta with_destruct with_evars
-      naming id lemma tac in
+    apply_in_delayed_once ~respect_opaque sidecond_first with_delta
+      with_destruct with_evars naming id lemma tac in
   Proofview.Goal.enter begin fun gl ->
   let destopt =
     if with_evars then MoveLast (* evars would depend on the whole context *)
@@ -2566,7 +2573,7 @@ let apply_in simple with_evars id lemmas ipat =
   general_apply_in false simple simple with_evars id lemmas ipat
 
 let apply_delayed_in simple with_evars id lemmas ipat =
-  general_apply_in false simple simple with_evars id lemmas ipat
+  general_apply_in ~respect_opaque:true false simple simple with_evars id lemmas ipat
 
 (*****************************)
 (* Tactics abstracting terms *)