3 files changed, 23 insertions, 20 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 218342efe4..cb54cac3f1 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -984,7 +984,9 @@ struct
 
   let parse_expr sigma parse_constant parse_exp ops_spec env term =
     if debug
-    then Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr term);
+    then (
+      let _, env = Pfedit.get_current_context () in
+      Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term));
 
 (*
     let constant_or_variable env term =
@@ -1103,9 +1105,10 @@ struct
     |  _ -> raise ParseError
 
 
-  let rconstant sigma term = 
+  let rconstant sigma term =
+    let _, env = Pfedit.get_current_context () in
     if debug
-    then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr term ++ fnl ());
+    then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ());
     let res = rconstant sigma term in
       if debug then 
 	(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1145,9 +1148,9 @@ struct
 
   let  parse_arith parse_op parse_expr env cstr gl =
     let sigma = gl.sigma in
-   if debug
-   then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ());
-   match EConstr.kind sigma cstr with
+    if debug
+    then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ());
+    match EConstr.kind sigma cstr with
     | Term.App(op,args) ->
        let (op,lhs,rhs) = parse_op gl (op,args) in
        let (e1,env) = parse_expr sigma env lhs in
@@ -1908,7 +1911,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
      let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
      let ff = dump_formula formula_typ
        (dump_cstr spec.typ spec.dump_coeff) ff in
-       Feedback.msg_notice (Printer.pr_leconstr ff);
+       Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff);
        Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
    end;
 
@@ -1932,9 +1935,9 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2
       Feedback.msg_notice (Pp.str "\nAFormula\n") ;
       let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
       let ff' = dump_formula formula_typ
-        (dump_cstr spec.typ spec.dump_coeff) ff' in
-        Feedback.msg_notice (Printer.pr_leconstr ff');
-        Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
+          (dump_cstr spec.typ spec.dump_coeff) ff' in
+      Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff');
+      Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
     end;
 
   (* Even if it does not work, this does not mean it is not provable
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 7da4a3b829..52c6ef983d 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' =
 
 (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **)
 
-let and_cnf f1 f2 =
-  app f1 f2
+let and_cnf =
+  app
 
 (** val xcnf :
     ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1
@@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
     'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
     -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **)
 
-let norm cO cI cplus ctimes cminus copp ceqb =
-  norm_aux cO cI cplus ctimes cminus copp ceqb
+let norm =
+  norm_aux
 
 (** val psub0 :
     'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
     -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
 
-let psub0 cO cplus cminus copp ceqb =
-  psub cO cplus cminus copp ceqb
+let psub0 =
+  psub
 
 (** val padd0 :
     'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
     -> 'a1 pol **)
 
-let padd0 cO cplus ceqb =
-  padd cO cplus ceqb
+let padd0 =
+  padd
 
 (** val xnormalise :
     'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 49ccb468c1..387a525141 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -149,7 +149,7 @@ let open_in f =
     match read_key_elem inch with
       | None -> ()
       | Some (key,elem) ->
-	  Table.add htbl key elem ;
+          Table.replace htbl key elem ;
 	  xload () in
     try
       (* Locking of the (whole) file while reading *)
@@ -195,7 +195,7 @@ let add t k e =
     else
       let fd = descr_of_out_channel outch in
       begin
-       Table.add tbl k e ;
+       Table.replace tbl k e ;
        do_under_lock Write fd 
         (fun _ -> 
          Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;