diff options
Diffstat (limited to 'src/trace/smt_tactic.ml4')
| -rw-r--r-- | src/trace/smt_tactic.ml4 | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/trace/smt_tactic.ml4 b/src/trace/smt_tactic.ml4 index 219810d..efac23b 100644 --- a/src/trace/smt_tactic.ml4 +++ b/src/trace/smt_tactic.ml4 @@ -14,6 +14,9 @@ (**************************************************************************) +(* Uncomment for 8.5 *) +(* DECLARE PLUGIN "SMTCoq_plugin" *) + VERNAC COMMAND EXTEND Parse_certif_zchaff | [ "Parse_certif_zchaff" ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] -> @@ -27,7 +30,7 @@ VERNAC COMMAND EXTEND Parse_certif_zchaff | [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] -> [ Zchaff.theorem name fdimacs fproof - ] + ] END VERNAC COMMAND EXTEND Parse_certif_verit @@ -46,6 +49,7 @@ VERNAC COMMAND EXTEND Parse_certif_verit ] END +(* Comment for 8.5 *) TACTIC EXTEND zchaff | [ "zchaff" ] -> [ Zchaff.tactic ] END |