diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:46:10 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:46:10 +0200 |
| commit | 3fac4bd6183b19e7980d9e0131dffa7a49f4c096 (patch) | |
| tree | 626ed0a12332262a8506cd56a5d31e00aea321cb /src/trace/coqTerms.ml | |
| parent | a5bd782f300c3767936fc3f45df6a09cda185370 (diff) | |
| download | smtcoq-3fac4bd6183b19e7980d9e0131dffa7a49f4c096.tar.gz smtcoq-3fac4bd6183b19e7980d9e0131dffa7a49f4c096.zip | |
The tactic "verit" generates more user-friendly subgoals
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 1cc6d4f..429ed72 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -85,6 +85,9 @@ let cNone = gen_constant init_modules "None" (* Pairs *) let cpair = gen_constant init_modules "pair" +(* Dependent pairs *) +let csigT = gen_constant init_modules "sigT" + (* Logical Operators *) let cnot = gen_constant init_modules "not" let ceq = gen_constant init_modules "eq" @@ -112,7 +115,6 @@ let ctyp_eqb = gen_constant smt_modules "typ_eqb" let cTyp_eqb = gen_constant smt_modules "Typ_eqb" let cte_carrier = gen_constant smt_modules "te_carrier" let cte_eqb = gen_constant smt_modules "te_eqb" -let ctyp_eqb_param = gen_constant smt_modules "typ_eqb_param" let ctyp_eqb_of_typ_eqb_param = gen_constant smt_modules "typ_eqb_of_typ_eqb_param" let cunit_typ_eqb = gen_constant smt_modules "unit_typ_eqb" |