aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-04-08 04:00:44 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-24 23:27:23 +0200
commit1f4beb7369a0462502b26476e8748f21cc92ef72 (patch)
tree6834b9ce39ca05787f38ac9f6ea3324b741e6cf3 /plugins/ltac
parent520c96f3af069e0af3ceb94fac6a1d8eb895a0a3 (diff)
[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.
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.ml46
1 files changed, 2 insertions, 4 deletions
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 *)