aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/coqTerms.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/coqTerms.ml')
-rw-r--r--src/trace/coqTerms.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index f2c24b8..a58fcfa 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -104,6 +104,8 @@ let smt_modules = [ ["SMTCoq";"Misc"];
["SMTCoq";"SMT_terms";"Atom"]
]
+let cState_C_t = gen_constant [["SMTCoq";"State";"C"]] "t"
+
let cdistinct = gen_constant smt_modules "distinct"
let ctype = gen_constant smt_modules "type"