aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-15 23:25:53 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-05 09:59:47 +0200
commitd28c22a7b173fc78de98c8bf0f986cb163e210a0 (patch)
tree7087075e4ebeab0c10a3339f5f55cc75fa98386f
parentf6538f1a7f8ad2bdc0bc446d4ca35078d55d63ee (diff)
Make direct invocations of `simple apply` obey `Opaque` directive.
When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
-rw-r--r--CHANGES3
-rw-r--r--plugins/ssrmatching/ssrmatching.ml48
-rw-r--r--pretyping/unification.ml9
-rw-r--r--pretyping/unification.mli3
-rw-r--r--tactics/tactics.ml45
5 files changed, 43 insertions, 25 deletions
diff --git a/CHANGES b/CHANGES
index e8718bbab..787c9ba12 100644
--- a/CHANGES
+++ b/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
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 93c63d522..b1c5e131f 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/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)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5f7faa13e..4c788abdb 100644
--- a/pretyping/unification.ml
+++ b/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;
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 16ce5c93d..e2e261ae7 100644
--- a/pretyping/unification.mli
+++ b/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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 58c62af85..78f4fcf92 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1638,13 +1638,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. *)
@@ -1653,7 +1651,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
@@ -1719,14 +1722,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
@@ -1801,14 +1804,12 @@ 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
@@ -1816,6 +1817,12 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
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
@@ -1835,14 +1842,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
@@ -2529,11 +2536,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 *)
@@ -2564,7 +2571,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 *)