From 1f4beb7369a0462502b26476e8748f21cc92ef72 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 8 Apr 2018 04:00:44 +0200 Subject: [tactics] Remove anonymous fix/cofix form. We remove the `fix N / cofix N` forms from the tactic language. This way, these tactics don't depend anymore on the proof context, in particular on the proof name, which seems like a fragile practice. Apart from the concerns wrt maintenability of proof scripts, this also helps making the "proof state" functional; as we don't have to propagate the proof name to the tactic layer. --- plugins/ltac/coretactics.ml4 | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'plugins/ltac') diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 931633e1a..faa9e413b 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -273,15 +273,13 @@ END (* Fix *) TACTIC EXTEND fix - [ "fix" natural(n) ] -> [ Tactics.fix None n ] -| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ] + [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ] -> [ Tactics.cofix None ] -| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ] + [ "cofix" ident(id) ] -> [ Tactics.cofix id ] END (* Clear *) -- cgit v1.2.3