Compiles with Coq-8.6

3 files changed, 10 insertions, 11 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
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 8f2fea8..1abea36 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -17,7 +17,6 @@
 open Util
 open SmtMisc
 open CoqTerms
-open Errors
 
 module type ATOM = 
   sig 
@@ -315,7 +314,7 @@ module Make (Atom:ATOM) =
               let l1 = mk_hform b1 in
               let l2 = mk_hform b2 in
               get reify (Fapp (Fimp, [|l1;l2|]))
-            | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+            | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
 	| CCifb ->
 	    (* We should also be able to reify if then else *)
 	    begin match args with
@@ -324,7 +323,7 @@ module Make (Atom:ATOM) =
 		let l2 = mk_hform b2 in
 		let l3 = mk_hform b3 in
 		get reify (Fapp(Fite, [|l1;l2;l3|]))
-	    | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+	    | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
 	    end
 	| _ -> 
 	    let a = atom_of_coq  h in
@@ -336,7 +335,7 @@ module Make (Atom:ATOM) =
 	    let l1 = mk_hform b1 in
             let l2 = mk_hform b2 in
             get reify (f [|l1; l2|])
-	| _ ->  error "SmtForm.Form.of_coq: wrong number of arguments"
+	| _ ->  Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
 	  
       and mk_fnot i args =
 	match args with
@@ -350,7 +349,7 @@ module Make (Atom:ATOM) =
               let l = if r = 0 then l else neg l in
 	      if q = 0 then l
 	      else get reify (Fapp(Fnot2 q, [|l|]))
-	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
 	  
       and mk_fand acc args = 
 	match args with
@@ -362,7 +361,7 @@ module Make (Atom:ATOM) =
 	    else 
 	      let l1 = mk_hform t1 in
 	      get reify (Fapp(Fand, Array.of_list  (l1::l2::acc)))
-	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for andb" 
+	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" 
 
       and mk_for acc args = 
 	match args with
@@ -374,7 +373,7 @@ module Make (Atom:ATOM) =
 	    else 
 	      let l1 = mk_hform t1 in
 	      get reify (Fapp(For, Array.of_list (l1::l2::acc)))
-	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
 
       let l = mk_hform c in
       l
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 74d3170..c372310 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -324,12 +324,12 @@ let to_coq to_lit interp (cstep,
           mklApp cEqCgrP [|out_c c; out_f f1; out_f f2; res|]
 	| LiaMicromega (cl,d) ->
           let cl' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
-          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in
+          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm; Micromega_plugin.Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm|]) in
           mklApp cLiaMicromega [|out_c c; cl'; c'|]
         | LiaDiseq l -> mklApp cLiaDiseq [|out_c c; out_f l|]
         | SplArith (orig,res,l) ->
           let res' = out_f res in
-          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in
+          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm; Micromega_plugin.Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm|]) in
           mklApp cSplArith [|out_c c; out_c orig; res'; l'|]
 	| SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|]
         | Hole (prem_id, concl) ->