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 /user-contrib | |
| 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 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 72df4d75c8..2102cd1172 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1290,7 +1290,7 @@ let () = let ist = Tac2interp.get_env ist in let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in let name, poly = Id.of_string "ltac2", poly in - let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma concl tac in + let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma concl tac in (EConstr.of_constr c, sigma) in GlobEnv.register_constr_interp0 wit_ltac2_constr interp diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index b84fd0b6d9..136ea8b7e0 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -902,7 +902,7 @@ let solve ~pstate default tac = let pstate, status = Declare.map_fold_proof_endline begin fun etac p -> let with_end_tac = if default then Some etac else None in let g = Goal_select.get_default_goal_selector () in - let (p, status) = Pfedit.solve g None tac ?with_end_tac p in + let (p, status) = Proof.solve g None tac ?with_end_tac p in (* in case a strict subtree was completed, go back to the top of the prooftree *) let p = Proof.maximal_unfocus Vernacentries.command_focus p in |