diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:30 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:36 -0500 |
| commit | f65b945119341ae8afa69bd0b7dc005c9fcc768b (patch) | |
| tree | c264125578d3b8edd752740701789f7b1e4e26bb /proofs/signatures | |
| parent | 53c301aa808218abe725014e01bddc19fe11a116 (diff) | |
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
Diffstat (limited to 'proofs/signatures')
| -rwxr-xr-x | proofs/signatures/th_quant.plf | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/proofs/signatures/th_quant.plf b/proofs/signatures/th_quant.plf index d85b2115c..e212f835d 100755 --- a/proofs/signatures/th_quant.plf +++ b/proofs/signatures/th_quant.plf @@ -14,10 +14,7 @@ (match ti ((apply si1 si2 ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff))) (default ff))) - (default - (match ti - ((apply si1 si2 ti1 ti2) ff) - (default (eqterm ti (ifmarked t k t))))))) + (default (eqterm ti (ifmarked t k t))))) (program is_inst_f ((fi formula) (f formula) (k term)) bool (match f |