diff options
| author | Pierre-Marie Pédrot | 2020-04-30 17:35:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:49 +0200 |
| commit | fcef4f7d643d40cb652580e507d7bda914e8b9f2 (patch) | |
| tree | 4702f08ea499ea1b00ad699ed4942dc880b53ae3 /plugins/ssr/ssrequality.ml | |
| parent | 86751a2069fd3360742d44dbe66c221894196ad6 (diff) | |
Further port SSReflect tactics to the new engine.
Diffstat (limited to 'plugins/ssr/ssrequality.ml')
| -rw-r--r-- | plugins/ssr/ssrequality.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 1a73bfded0..33a2eb85d9 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -66,6 +66,8 @@ let simpltac = function | SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (Proofview.V82.of_tactic (donetac n))) | Nop -> tclIDTAC +let simpltac s = Proofview.V82.tactic ~nf_evars:false (simpltac s) + (** The "congr" tactic *) let interp_congrarg_at ist gl n rf ty m = @@ -197,7 +199,7 @@ let simplintac occ rdx sim gl = CErrors.user_err (Pp.str "Custom simpl tactic does not support patterns"); if occ <> None then CErrors.user_err (Pp.str "Custom simpl tactic does not support occurrence numbers"); - simpltac (Simpl m) gl + Proofview.V82.of_tactic (simpltac (Simpl m)) gl end else let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in @@ -207,7 +209,7 @@ let simplintac occ rdx sim gl = match sim with | Simpl m -> simptac m gl | SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (Proofview.V82.of_tactic (donetac n))) gl - | _ -> simpltac sim gl + | _ -> Proofview.V82.of_tactic (simpltac sim) gl let rec get_evalref env sigma c = match EConstr.kind sigma c with | Var id -> EvalVarRef id @@ -627,7 +629,9 @@ let ssrinstancesofrule ist dir arg = with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl end -let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl +let ipat_rewrite occ dir c = Proofview.V82.tactic ~nf_evars:false begin fun gl -> + rwrxtac occ None dir (project gl, c) gl +end let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl = let fail = ref false in |