aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/cctac.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 204af93d56..ab53fec6f2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -34,11 +34,11 @@ let _f_equal = constant ["Init";"Logic"] "f_equal"
let _eq_rect = constant ["Init";"Logic"] "eq_rect"
-let _refl_equal = constant ["Init";"Logic"] "refl_equal"
+let _refl_equal = constant ["Init";"Logic"] "eq_refl"
-let _sym_eq = constant ["Init";"Logic"] "sym_eq"
+let _sym_eq = constant ["Init";"Logic"] "eq_sym"
-let _trans_eq = constant ["Init";"Logic"] "trans_eq"
+let _trans_eq = constant ["Init";"Logic"] "eq_trans"
let _eq = constant ["Init";"Logic"] "eq"