diff options
| author | Pierre-Marie Pédrot | 2016-05-13 00:16:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 21:17:24 +0200 |
| commit | 73cdb000ec07ec484557839c4b94fcf779df2f06 (patch) | |
| tree | 4aa04d713d26b537c187e1be801b4788d4a4e915 /proofs/proof_type.mli | |
| parent | cead0ce54cf290016e088ee7f203d327a3eea957 (diff) | |
Put the "clear" tactic into the monad.
Diffstat (limited to 'proofs/proof_type.mli')
| -rw-r--r-- | proofs/proof_type.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index b4c9dae2a3..48ad50c7a0 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -22,7 +22,6 @@ type prim_rule = | FixRule of Id.t * int * (Id.t * int * constr) list * int | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr - | Thin of Id.t list | Move of Id.t * Id.t move_location (** Nowadays, the only rules we'll consider are the primitive rules *) |