diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-26 18:35:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-27 19:17:37 +0200 |
| commit | 3c1c101a8757c438379441a334f31f5fe656ef55 (patch) | |
| tree | 4f029a6d586337bd25b09ce77afe7705a01c8c6f /tactics/dnet.ml | |
| parent | a7946816d96cb66aa7d62302e8aa602a3a9f3c99 (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 'tactics/dnet.ml')
0 files changed, 0 insertions, 0 deletions