aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Case2.v
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-07-20 11:33:40 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-07-20 11:33:40 +0200
commitd8cd9ba6d56d32eb8aa383bca9198a18517e82d3 (patch)
treedc6670607c7831c5a6b80da427b1f299ffd0f2df /test-suite/failure/Case2.v
parent2de309b65b379a3c496752aa25f1cfc177644222 (diff)
parente2e23a52655fbd04a1cc659e64fb520d97d7f9db (diff)
Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.
Diffstat (limited to 'test-suite/failure/Case2.v')
0 files changed, 0 insertions, 0 deletions