diff options
| author | Emilio Jesus Gallego Arias | 2018-11-16 20:16:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-21 01:26:45 +0100 |
| commit | 417641e48129c9ba8656c622c9b64cd32641e7de (patch) | |
| tree | bbd47886f4649999ecad9f21ffb6ff55869f0132 /proofs/logic.mli | |
| parent | 968be14b3788e112425eedf696f2e5e35d35ba17 (diff) | |
[legacy proof engine] Remove some cruft.
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
Diffstat (limited to 'proofs/logic.mli')
| -rw-r--r-- | proofs/logic.mli | 19 |
1 files changed, 6 insertions, 13 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli index 2cad278e10..f99076db23 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -13,27 +13,20 @@ open Names open Constr open Evd -open Proof_type -(** This suppresses check done in [prim_refiner] for the tactic given in - argument; works by side-effect *) - -val with_check : tactic -> tactic - -(** [without_check] respectively means:\\ - [Intro]: no check that the name does not exist\\ - [Intro_after]: no check that the name does not exist and that variables in +(** [check] respectively means:\\ + [Intro]: check that the name does not exist\\ + [Intro_after]: check that the name does not exist and that variables in its type does not escape their scope\\ - [Intro_replacing]: no check that the name does not exist and that + [Intro_replacing]: check that the name does not exist and that variables in its type does not escape their scope\\ [Convert_hyp]: - no check that the name exist and that its type is convertible\\ + check that the name exist and that its type is convertible\\ *) (** The primitive refiner. *) -val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map - +val prim_refiner : check:bool -> constr -> evar_map -> Goal.goal -> Goal.goal list * evar_map (** {6 Refiner errors. } *) |