aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-26 18:35:48 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-03-27 19:17:37 +0200
commit3c1c101a8757c438379441a334f31f5fe656ef55 (patch)
tree4f029a6d586337bd25b09ce77afe7705a01c8c6f /INSTALL
parenta7946816d96cb66aa7d62302e8aa602a3a9f3c99 (diff)
Adding tacticals tclBINDFIRST/tclBINDLAST.
Design choice: Failing with an anomaly or with a catchable Ltac error "Fail": we fail with a Fail as it was the case with the related constrained version of tclTHENFIRST/tclTHENLAST.
Diffstat (limited to 'INSTALL')
0 files changed, 0 insertions, 0 deletions