diff options
| author | Quentin Garchery <garchery.quentin@gmail.com> | 2018-10-27 20:08:44 +0200 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2018-10-28 00:39:25 +0200 |
| commit | faaa2848c37444f8f37ac432c25f9f813e1df39b (patch) | |
| tree | 2672d165fd13b5262005406d1496bc6a14e8b521 /src/trace/coqTerms.ml | |
| parent | 7940ef63c654be26b41ce20162207f3c67d0b10a (diff) | |
| download | smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.tar.gz smtcoq-faaa2848c37444f8f37ac432c25f9f813e1df39b.zip | |
Adding support for lemmas in the command verit
Diffstat (limited to 'src/trace/coqTerms.ml')
| -rw-r--r-- | src/trace/coqTerms.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 1874d5f..96d5a69 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -90,6 +90,8 @@ let csigT = gen_constant init_modules "sigT" let cnot = gen_constant init_modules "not" let ceq = gen_constant init_modules "eq" let crefl_equal = gen_constant init_modules "eq_refl" +let cconj = gen_constant init_modules "conj" +let cand = gen_constant init_modules "and" (* SMT_terms *) @@ -179,7 +181,7 @@ let make_certif_ops modules args = gen_constant"ImmBuildDef2", gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP", gen_constant "LiaMicromega", gen_constant "LiaDiseq", gen_constant "SplArith", gen_constant "SplDistinctElim", - gen_constant "Hole") + gen_constant "Hole", gen_constant "ForallInst") (** Useful construction *) |