From b6d7acb9a033ecb0f7e75ba358d9a748eb0f580f Mon Sep 17 00:00:00 2001 From: Leon Gondelman Date: Wed, 8 Feb 2017 16:53:53 +0100 Subject: [PATCH] coercions wip --- src/core/coercion.ml | 1 + src/core/theory.ml | 1 + 2 files changed, 2 insertions(+) diff --git a/src/core/coercion.ml b/src/core/coercion.ml index afe0c0e76..3ef69cd03 100644 --- a/src/core/coercion.ml +++ b/src/core/coercion.ml @@ -74,6 +74,7 @@ let rec add_crc crcmap crc trans = Mts.fold (close_right crc) m1 crcmap_uc1 in Mts.fold (close_left_right) crcmap_uc2 crcmap_uc2 + let add crcmap ls = let c = create_crc ls in add_crc crcmap c true diff --git a/src/core/theory.ml b/src/core/theory.ml index 3af56eac6..d5119e2bd 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -284,6 +284,7 @@ let empty_theory n p = { let close_theory uc = match uc.uc_export with | [e] -> + Coercion.print uc.uc_crcmap; { th_name = uc.uc_name; th_path = uc.uc_path; th_decls = List.rev uc.uc_decls; -- GitLab