diff options
| author | Pierre-Marie Pédrot | 2020-04-30 15:57:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 13:09:49 +0200 |
| commit | 1109581ba7afca804515fc6179565da808bae4f7 (patch) | |
| tree | fe6941fcf9e44d60f2902cb5f732fe6a80955ea9 /plugins | |
| parent | 04a8c766a51b17997d8a9ffcf6f2d7beffc599ce (diff) | |
Wrap Refiner.refiner in the tactic monad.
This function was used almost everywhere with the wrapper around.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 5 | ||||
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 |
3 files changed, 6 insertions, 3 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 7b2ce671a3..f4200854c2 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -41,7 +41,10 @@ let observe_tac s = observe_tac (fun _ _ -> Pp.str s) let finish_proof dynamic_infos g = observe_tac "finish" (Proofview.V82.of_tactic assumption) g -let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c) +let refine c = + Proofview.V82.of_tactic + (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)) + let thin l = Proofview.V82.of_tactic (Tactics.clear l) let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 134a9e4b36..95a0790ff3 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1014,7 +1014,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t g pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); Proofview.(V82.of_tactic (Tacticals.New.tclTHENLIST [ - V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t)); + Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t); (if first_goes_last then cycle 1 else tclUNIT ()) ])) gl diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index b44600a8cf..8f445b4397 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -477,7 +477,7 @@ let revtoptac n0 gl = let dc, cl = EConstr.decompose_prod_n_assum (project gl) n (pf_concl gl) in let dc' = dc @ [Context.Rel.Declaration.LocalAssum(make_annot (Name rev_id) Sorts.Relevant, EConstr.it_mkProd_or_LetIn cl (List.rev dc))] in let f = EConstr.it_mkLambda_or_LetIn (mkEtaApp (EConstr.mkRel (n + 1)) (-n) 1) dc' in - Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|]))) gl + Proofview.V82.of_tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr (EConstr.mkApp (f, [|Evarutil.mk_new_meta ()|])))) gl let equality_inj l b id c gl = let msg = ref "" in |