diff options
author | 2018-02-26 18:35:48 +0100 | |
---|---|---|
committer | 2018-03-27 19:17:37 +0200 | |
commit | 3c1c101a8757c438379441a334f31f5fe656ef55 (patch) | |
tree | 4f029a6d586337bd25b09ce77afe7705a01c8c6f /test-suite/prerequisite/bind_univs.v | |
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 'test-suite/prerequisite/bind_univs.v')
0 files changed, 0 insertions, 0 deletions