From 48e123caddd6a4c4edd60d8f39b78a5421418f40 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 3 Oct 2017 11:20:59 +0200 Subject: Compiles with both versions of Coq --- src/trace/smtCertif.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/trace/smtCertif.ml') diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml index 868a311..e4ed262 100644 --- a/src/trace/smtCertif.ml +++ b/src/trace/smtCertif.ml @@ -99,11 +99,11 @@ type 'hform rule = *) (* Linear arithmetic *) - | LiaMicromega of 'hform list * Micromega_plugin.Certificate.Mc.zArithProof list + | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list | LiaDiseq of 'hform (* Arithmetic simplifications *) - | SplArith of 'hform clause * 'hform * Micromega_plugin.Certificate.Mc.zArithProof list + | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list (* Elimination of operators *) | SplDistinctElim of 'hform clause * 'hform -- cgit