aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtCertif.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/trace/smtCertif.ml')
-rw-r--r--src/trace/smtCertif.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index f39bff4..868a311 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -99,11 +99,11 @@ type 'hform rule =
*)
(* Linear arithmetic *)
- | LiaMicromega of 'hform list * Certificate.Mc.zArithProof list
+ | LiaMicromega of 'hform list * Micromega_plugin.Certificate.Mc.zArithProof list
| LiaDiseq of 'hform
(* Arithmetic simplifications *)
- | SplArith of 'hform clause * 'hform * Certificate.Mc.zArithProof list
+ | SplArith of 'hform clause * 'hform * Micromega_plugin.Certificate.Mc.zArithProof list
(* Elimination of operators *)
| SplDistinctElim of 'hform clause * 'hform