diff options
| author | Pierre-Marie Pédrot | 2018-09-25 10:43:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-25 10:43:57 +0200 |
| commit | 7eb8a7eb8d23ffaf149f71a46fb1b089b90db7f8 (patch) | |
| tree | aa480ca16c64e5c1e04ac31dd9bc8066f44840c1 /plugins/micromega | |
| parent | 4ae5a0e2dec60f753d21385b88991a9d1f0ec62d (diff) | |
| parent | 6b61b63bb8626827708024cbea1312a703a54124 (diff) | |
Merge PR #6343: [engine] Remove and deprecate `nf_enter` et al.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index f22147f8b0..e0a369ca5f 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1456,7 +1456,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) (vm_of_list env) in (* todo : directly generate the proof term - or generalize before conversion? *) - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.tclTHENLIST [ Tactics.change_concl @@ -1709,7 +1709,7 @@ let micromega_gen (normalise:'cst atom -> 'cst mc_cnf) unsat deduce spec dumpexpr prover tac = - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in @@ -1787,7 +1787,7 @@ let micromega_order_changer cert env ff = let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) (vm_of_list env) in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> Tacticals.New.tclTHENLIST [ (Tactics.change_concl @@ -1817,7 +1817,7 @@ let micromega_genr prover tac = proof_typ = Lazy.force coq_QWitness ; dump_proof = dump_psatz coq_Q dump_q } in - Proofview.Goal.nf_enter begin fun gl -> + Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let concl = Tacmach.New.pf_concl gl in let hyps = Tacmach.New.pf_hyps_types gl in |