diff options
| author | Maxime Dénès | 2017-08-29 14:37:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-29 14:37:55 +0200 |
| commit | 751246d893470b95d3d96ef87fe6dc86950d8d63 (patch) | |
| tree | a4512b9db59c10ed761d124f63f18a30ce1f51aa /proofs/proof_type.ml | |
| parent | 7e29b535397c98a46999ecdd827fa5f4cebc8798 (diff) | |
| parent | 4f392bc8114309f388791c1ddc7cc95cc021aa5e (diff) | |
Merge PR #830: Moving assert (the "Cut" rule) to new proof engine
Diffstat (limited to 'proofs/proof_type.ml')
| -rw-r--r-- | proofs/proof_type.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 11f1a13e6e..2ad5f607f2 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -9,14 +9,12 @@ (** Legacy proof engine. Do not use in newly written code. *) open Evd -open Names open Term (** This module defines the structure of proof tree and the tactic type. So, it is used by [Proof_tree] and [Refiner] *) type prim_rule = - | Cut of bool * bool * Id.t * types | Refine of constr (** Nowadays, the only rules we'll consider are the primitive rules *) |