aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-02-14 09:07:46 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-03-04 18:01:24 +0100
commit7267e31fa4456aee62a1e39dfdb7e38a8832f93f (patch)
treea625725414aa13313b8c09e65f1fa875f9f780f0
parentf7153351bc1d4af2f402671c4937a5186ba77fc3 (diff)
ssr: ipats: V82.tactic ~nf_evars:false everywhere
-rw-r--r--plugins/ssr/ssrbwd.ml14
-rw-r--r--plugins/ssr/ssrelim.ml9
-rw-r--r--plugins/ssr/ssrelim.mli5
-rw-r--r--plugins/ssr/ssripats.ml36
4 files changed, 35 insertions, 29 deletions
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index daad730ff..23da1eb69 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -121,13 +121,13 @@ let refine_interp_apply_view dbl ist gl gv =
else [])
let apply_top_tac =
- Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (introid top_id);
- Proofview.V82.tactic (apply_rconstr (mkRVar top_id));
- Tactics.clear [top_id]
+ Tacticals.tclTHENLIST [
+ introid top_id;
+ apply_rconstr (mkRVar top_id);
+ old_cleartac [SsrHyp(None,top_id)]
]
-let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic (fun gl ->
+let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic ~nf_evars:false (fun gl ->
let _, clr = interp_hyps ist gl gclr in
let vtac gv i gl' = refine_interp_apply_view i ist gl' gv in
let ggenl, tclGENTAC =
@@ -152,7 +152,7 @@ let inner_ssrapplytac gviews (ggenl, gclr) ist = Proofview.V82.tactic (fun gl ->
let gl = pf_merge_uc_of sigma gl in
Tacticals.tclTHENLIST [old_cleartac clr; refine_with ~beta:true lemma; old_cleartac clr'] gl
| _, _ ->
- let open Proofview.Notations in
- Proofview.V82.of_tactic (apply_top_tac <*> cleartac clr) gl) gl
+ Tacticals.tclTHENLIST [apply_top_tac; old_cleartac clr] gl) gl
)
+let apply_top_tac = Proofview.V82.tactic ~nf_evars:false apply_top_tac
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index b3e59f7fc..a5d44d925 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -377,7 +377,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac
let no_intro ?ist what eqid elim_tac is_rec clr = elim_tac
let elimtac x =
- Proofview.V82.tactic
+ Proofview.V82.tactic ~nf_evars:false
(ssrelim ~is_case:false [] (`EConstr ([],None,x)) None no_intro)
let casetac x = ssrelim ~is_case:true [] (`EConstr ([],None,x)) None no_intro
@@ -435,6 +435,9 @@ let perform_injection c gl =
let injtac = Tacticals.tclTHEN (introid id) (injectidl2rtac id id_with_ebind) in
Tacticals.tclTHENLAST (Proofview.V82.of_tactic (Tactics.apply (EConstr.compose_lam dc cl1))) injtac gl
-let ssrscasetac force_inj c = Proofview.V82.tactic (fun gl ->
- if force_inj || is_injection_case c gl then perform_injection c gl
+let ssrscase_or_inj_tac c = Proofview.V82.tactic ~nf_evars:false (fun gl ->
+ if is_injection_case c gl then perform_injection c gl
else casetac c gl)
+
+let ssrscasetac c =
+ Proofview.V82.tactic ~nf_evars:false (fun gl -> casetac c gl)
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli
index b802486a0..0541a13ed 100644
--- a/plugins/ssr/ssrelim.mli
+++ b/plugins/ssr/ssrelim.mli
@@ -45,6 +45,9 @@ val perform_injection :
Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
val ssrscasetac :
- bool ->
+ EConstr.constr ->
+ unit Proofview.tactic
+
+val ssrscase_or_inj_tac :
EConstr.constr ->
unit Proofview.tactic
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 77ebe17a4..1a964bd50 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -137,9 +137,9 @@ let tac_case t =
Ssrcommon.tacTYPEOF t >>= fun ty ->
Ssrcommon.tacIS_INJECTION_CASE ~ty t >>= fun is_inj ->
if is_inj then
- V82.tactic (Ssrelim.perform_injection t)
+ V82.tactic ~nf_evars:false (Ssrelim.perform_injection t)
else
- Ssrelim.ssrscasetac false t
+ Ssrelim.ssrscasetac t
end
(** [=> [: id]] ************************************************************)
@@ -218,7 +218,7 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss
| IPatInj ipatss ->
tclIORPAT (Ssrcommon.tclWITHTOP
- (fun t -> V82.tactic (Ssrelim.perform_injection t))) ipatss
+ (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) ipatss
| IPatAnon Drop -> intro_drop
| IPatAnon One -> Ssrcommon.tclINTRO_ANON
@@ -230,15 +230,15 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
| IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
| IPatSimpl (Simpl n) ->
- V82.tactic (Ssrequality.simpltac (Simpl n))
+ V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
| IPatSimpl (Cut n) ->
- V82.tactic (Ssrequality.simpltac (Cut n))
+ V82.tactic ~nf_evars:false (Ssrequality.simpltac (Cut n))
| IPatSimpl (SimplCut (n,m)) ->
- V82.tactic (Ssrequality.simpltac (SimplCut (n,m)))
+ V82.tactic ~nf_evars:false (Ssrequality.simpltac (SimplCut (n,m)))
| IPatRewrite (occ,dir) ->
Ssrcommon.tclWITHTOP
- (fun x -> V82.tactic (Ssrequality.ipat_rewrite occ dir x))
+ (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x))
| IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids
@@ -302,7 +302,7 @@ end
let with_dgens { dgens; gens; clr } maintac = match gens with
| [] -> with_defective maintac dgens clr
| gen :: gens ->
- V82.tactic (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen
+ V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) <*> maintac dgens gen
let mkCoqEq env sigma =
let eq = Coqlib.((build_coq_eq_data ()).eq) in
@@ -326,7 +326,7 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr =
| Term.ProdType (_, src, tgt) -> begin
match EConstr.kind_of_type sigma src with
| Term.AtomicType (hd, _) when Ssrcommon.is_protect hd env sigma ->
- V82.tactic Ssrcommon.unprotecttac <*>
+ V82.tactic ~nf_evars:false Ssrcommon.unprotecttac <*>
Ssrcommon.tclINTRO_ID ipat
| _ -> Ssrcommon.tclINTRO_ANON <*> intro_eq ()
end
@@ -380,9 +380,9 @@ let elim_intro_tac ipats ?ist what eqid ssrelim is_rec clr =
| _ -> tclUNIT () in
let unprot =
if eqid <> None && is_rec
- then V82.tactic Ssrcommon.unprotecttac else tclUNIT () in
+ then V82.tactic ~nf_evars:false Ssrcommon.unprotecttac else tclUNIT () in
V82.of_tactic begin
- V82.tactic ssrelim <*>
+ V82.tactic ~nf_evars:false ssrelim <*>
tclIPAT_EQ (intro_eq <*> unprot) ipats
end
@@ -477,12 +477,12 @@ let ssrelimtac (view, (eqid, (dgens, ipats))) =
| [v] ->
Ssrcommon.tclINTERP_AST_CLOSURE_TERM_AS_CONSTR v >>= fun cs ->
tclDISPATCH (List.map (fun elim ->
- V82.tactic
+ V82.tactic ~nf_evars:false
(Ssrelim.ssrelim deps (`EGen gen) ~elim eqid (elim_intro_tac ipats)))
cs)
| [] ->
tclINDEPENDENT
- (V82.tactic
+ (V82.tactic ~nf_evars:false
(Ssrelim.ssrelim deps (`EGen gen) eqid (elim_intro_tac ipats)))
| _ ->
Ssrcommon.errorstrm
@@ -497,7 +497,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) =
Ssrcommon.tacIS_INJECTION_CASE vc >>= fun inj ->
let simple = (eqid = None && deps = [] && occ = None) in
if simple && inj then
- V82.tactic (Ssrelim.perform_injection vc) <*>
+ V82.tactic ~nf_evars:false (Ssrelim.perform_injection vc) <*>
Tactics.clear (List.map Ssrcommon.hyp_id clear) <*>
tclIPATssr ipats
else
@@ -506,7 +506,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) =
if view <> [] && eqid <> None && deps = []
then [gen], [], None
else deps, clear, occ in
- V82.tactic
+ V82.tactic ~nf_evars:false
(Ssrelim.ssrelim ~is_case:true deps (`EConstr (clear, occ, vc))
eqid (elim_intro_tac ipats))
in
@@ -515,7 +515,7 @@ let ssrcasetac (view, (eqid, (dgens, ipats))) =
in
with_dgens dgens (ndefectcasetac view eqid ipats)
-let ssrscasetoptac = Ssrcommon.tclWITHTOP (Ssrelim.ssrscasetac false)
+let ssrscasetoptac = Ssrcommon.tclWITHTOP Ssrelim.ssrscase_or_inj_tac
let ssrselimtoptac = Ssrcommon.tclWITHTOP Ssrelim.elimtac
(** [move] **************************************************************)
@@ -555,7 +555,7 @@ let tclIPAT ip =
let ssrmovetac = function
| _::_ as view, (_, ({ gens = lastgen :: gens; clr }, ipats)) ->
- let gentac = V82.tactic (Ssrcommon.genstac (gens, [])) in
+ let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, [])) in
let conclusion _ t clear ccl =
Tactics.apply_type ~typecheck:true ccl [t] <*>
Tactics.clear (List.map Ssrcommon.hyp_id clear) in
@@ -569,7 +569,7 @@ let ssrmovetac = function
let dgentac = with_dgens dgens eqmovetac in
dgentac <*> tclIPAT (eqmoveipats pat ipats)
| _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) ->
- let gentac = V82.tactic (Ssrcommon.genstac (gens, clr)) in
+ let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in
gentac <*> tclIPAT ipats
| _, (_, ({ clr }, ipats)) ->
Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats]