From 714256f7dcc68642117013dfa7b3ff8a76e468b9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 22 Nov 2014 15:12:28 +0100 Subject: Removing useless flag of the historical move tactic. --- proofs/proof_type.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/proof_type.ml') diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 613f85a73..bc3b1596b 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -32,7 +32,7 @@ type prim_rule = | Cofix of Id.t * (Id.t * constr) list * int | Refine of constr | Thin of Id.t list - | Move of bool * Id.t * Id.t move_location + | Move of Id.t * Id.t move_location (** Nowadays, the only rules we'll consider are the primitive rules *) -- cgit v1.2.3