diff options
| author | Emilio Jesus Gallego Arias | 2020-04-03 00:54:53 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-15 11:12:39 -0400 |
| commit | 28fc9aff20c39a04ad0e58e1bb8ec52c13631b61 (patch) | |
| tree | 3895a0ad5d966d53d66cfcb54c0e2c24474ea9c9 /plugins | |
| parent | 4a9d1b4b190e2cb3fb034882a703aa54c5059035 (diff) | |
[proof] Merge `Pfedit` into proofs.
If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index c2023289a4..7ed733cf57 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -346,7 +346,7 @@ open Vars let constr_flags () = { Pretyping.use_typeclasses = Pretyping.UseTC; - Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); + Pretyping.solve_unification_constraints = Proof.use_unification_heuristics (); Pretyping.fail_evar = false; Pretyping.expand_evars = true; Pretyping.program_mode = false; diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 0a46522543..3cc8c4934a 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -369,7 +369,7 @@ let vernac_solve ~pstate n info tcom b = let global = match n with SelectAll | SelectList _ -> true | _ -> false in let info = Option.append info (print_info_trace ()) in let (p,status) = - Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p + Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p in (* in case a strict subtree was completed, go back to the top of the prooftree *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 321b05b97c..820063c25c 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -639,7 +639,7 @@ let solve_remaining_by env sigma holes by = let env = Environ.reset_with_named_context evi.evar_hyps env in let ty = evi.evar_concl in let name, poly = Id.of_string "rewrite", false in - let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in + let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma ty solve_tac in Evd.define evk (EConstr.of_constr c) sigma in List.fold_left solve sigma indep diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b0e26e1def..dda7f0742c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2070,7 +2070,7 @@ let _ = *) let name, poly = Id.of_string "ltac_gen", poly in let name, poly = Id.of_string "ltac_gen", poly in - let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in + let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in (EConstr.of_constr c, sigma) in GlobEnv.register_constr_interp0 wit_tactic eval |